Method paste

basex-core/src/main/java/org/basex/gui/text/TextPanel.java:730–735

Pastes a string. @param string string to be pasted

(final String string)

   * @param string string to be pasted
   */
  private void paste(final String string) {
    final int pos = editor.pos();
    if(editor.isSelected()) editor.delete();
    editor.insert(string);
    finish(pos);
  }

  /**
   * Copies the selected text to the clipboard.