public void append(String str)
  {
    int newsize = this.size + str.length();

    // If there's insufficient capacity, make a new array
    if (newsize >= this.contents.length)
      {
        char[] oldcontents = this.contents;
        this.contents = new char[computeCapacity(newsize)];
        for (int i = 0; i < this.size; i++)
          this.contents[i] = oldcontents[i];
      } // if

    // Copy the characters.
    for (int i = this.size; i < newsize; i++)
      this.contents[i] = str.charAt(i - this.size);

    // Update the size
    this.size = newsize;
  } // append(String)