manage hyperlinks via PIDE editor interface;

tuned whitespace;

prefer PIDE editor operations; apply_query: insist in non-outdated snapshot via editor.current_command; tuned signature;

central management of Document.Overlays, independent of Document_Model;

tuned -- use Multi_Map;

support for maps with multiple entries per key;

tuned signature;

tuned signature;

tuned signature;

tuned signature -- more abstract PIDE editor operations;

tuned messages

clarified option name (since case/fold/rec are also destructors)

define case constant from other 'free constructor' axioms

introduced case tactics

tuning

handle both TVars and TFrees -- necessary for 'wrap_free_constructors'

qualify map and rel names

reverted ill-advised naming scheme of 5a77edcdbe54

made (hopefully temporary) hack more robust

added warning

gracefully handle one more error condition

gracefully fail to define polymorphic (co)datatypes in local context

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;