retain current task priority, to avoid distortion due to local forks (e.g. sledgehammer query operation);

removed "Locate" button, to avoid confusion about the slightly odd meaning of current_command with explicit theory context;

enable search in pre-loaded theory;

more GUI options;

tuned signature;

tuned;

tuned GUI;

tuned name generation code (to make it easier to adapt later)

honor user type names if possible

merged;

more abstract consume_status operation;

separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;

more active "provers" field, which increases chances that its history is stored;

removed command location is considered finished, and its overlay removed eventually; apply_query: empty output;

cancel_query via direct access to the exec_id of the running query process;

retain original messages properties, e.g. for retrieval via Command.Results;

clarified toplevel_error: absorb and print interrupts; tuned;

more explicit error;

tuned message;

removed unused YXML_Find_Theorems and Legacy_XML_Syntax;

more robust read_query; avoid pointless position, which is always line 1 for single-line input;

removed commented out declaration

tuned

merged

eliminate \<twosuperior> as well;

more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;

prefer plain subscript for identifiers;

proper low-level comparison -- heed warning by Scala compiler;

merged

prefer Code.abort with explicit error message