public void replaceText (String text, int start, int end)
public void replaceText (String str, int start, int end)
  public void replaceText (String text, int start, int end)  {    replaceRange (text, start, end);  }