normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>; tuned naming; dropped dead parameters;

tuned GUI;

clarified detach_operation: ignore empty output;

bounce focus back to main text area -- Output is for output, not query input;

update for release;

merged

tuned message;

no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;

some position markup to help locating the query context, e.g. from "Info" dockable;

tuned GUI;

tuned GUI;

tuned GUI;

tuned message: more compact, imitate actual command line;

enable "PIDE" docking framework by default, and rely on its "Detach" menu item;

some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;

untyped, unscoped, unchecked access to JVM objects;

Documented new property

generate 'map_ident' theorem for BNFs

explicit option to build library, which takes most of the time; produce minimal index, e.g. for test web page;

NEWS;

merged

more symbols; tuned proofs;

tuned message: "step" goes back to TTY mode before Proof General, while "depth" is more informative but sometimes confusing due to implementation details;

print results as "state", to avoid intrusion into the source text; print new local theory (again);

run commands as interactive, again after long history of fluctuation (9e196062bf88, 173974e07dea, e07dacec79e7) and quite different infrastructure for print tasks;

discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;

more emphatic output for Proof General;

tuned;

tuned defaults;

tuned message -- more context for detached window etc.;

tuned signature;

avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.

tuned GUI for Windows L&F;

clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;

tuned GUI layout;

clarified GUI events, e.g. relevant for insert via completion;

more robust line_range, according to usual jEdit confusion at end of last line (see also 71c5d1f516c0);

common support for search field, which is actually a light-weight Highlighter;

clarified GUI focus;

more uniform detach button;

tuned signature;

renamed "Find" to "Query", with more general operations;

hardwired default_frequency to avoid fluctuation of popup content;

more visual feedback on path_completion, at the risk of file-system access in GUI painting;

tuned;

explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";

tuned GUI layout;

tuned;

some complication with ListView.Renderer to get tooltips;

expose interrupts more like ML version, but not in managed bash processes of Build;

merged

uniform Toplevel.print for all proof commands;

clarified print operations for "terms" and "theorems";

more print operations; preserve declaration order;

tuned GUI;

more decisive change of focus; more explicit Print_Item with description;

support print operations as asynchronous query;

allow empty original, e.g. path "";

more robust process kill -- postpone interrupts on current thread;

tuned signature;