made code more robust

avoid DUP exception in local context (cf. 062aa11e98e1)

honor user tfree names

prefer local facts over global ones

use local context for name space

explicit "strict" flag for print functions (flipped internal meaning); non-strict query operations may operate on failed states;

avoid unnecessary case distinction

adjust tooltip for duplicates option

merged

NEWS;

Find is docked on startup;

sorted lines;

tuned GUI;

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

avoid re-inventing transitive closure

merged

theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map

tuned

tuned tactic;

abort execution of generated code with explicit exception message

merged

dockable window for Sledgehammer, based on asynchronous/parallel query operation;

tuned imports;

snippet for instr type

filter function on streams

tuned

tuned proofs;