observe extra line spacing for output as well;

persistent protocol_status, to improve performance of node_status a little;

more uniform painting of caret, which also improves visibility in invisible state;

tuned rendering -- visual indication of the status range, to make more clear when information might is out of view;

tuned for-comprehensions -- less structure mapping;

some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);

more direct command states -- merge_results is hardly ever needed;

unused;

more frugal command_status, which is often used in a tight loop;

simplified using "value class";

more precise BNF bound for datatypes

compile

tuning

added new-style (co)datatype interpretation hook

added BNF interpretation hook

added 'ctr_sugar' interpretation hook

tuned

merged

cumulative NEWS;

observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;

clear active areas (notably mouse pointer) before changing context (e.g. via hyperlink);

reset mouse pointer more decisively, for the sake of Mac OS X (despite the builtin policie of jEdit);

proper structural hashCode, which is required for Command.File equals (NB: Array has physical object identity);

tuned output;

tuned signature -- more static typing;

store blob content within document node: aux. files that were once open are made persistent; proper structural equality for Command.File and Symbol.Index;

some shortcuts for chunks, which sometimes avoid bulky string output;

support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;

tuned proofs

add complex_of_real coercion

add limits of power at top and bot

add connected_local_const

add rules about infinity of intervals

tuned proofs;

immediate completion even with delay, which is the default according to 638b29331549;

special treatment for various kinds of selections: imitate normal flow of editing;

merged

do not absorb vacuous copy operation, e.g. relevant when tooltip has focus but no selection, while the main text area has a selection but no focus;

check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;

dismiss all popups on mouse drags, e.g. to avoid conflict of C-hover of Isabelle/jEdit and C-selection of jEdit;

tuned proofs

minimized imports

merged

tuned rendering -- change mouse pointer for active areas;

propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save); tuned signature;

tuned signature;

tuned signature;

tuned -- see Text.Range.overlaps(Range);

tuned

tuned;

merged

tuned -- avoid code duplication;

tuned;

more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);

back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);

tuned;

redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands); more explicit ML_Compiler.flags;

clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;

more frugal merge of markup trees: non-overlapping tree counts as empty;

more frugal merge of markup trees: filter wrt. subsequent query;

tuned signature;

more careful treatment of multiple command states (eval + prints): merge content that is actually required; more standard Markup_Tree merge, including trivial cases;

tuned signature -- expose less intermediate information;

support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);

less markup by default -- this is stored persistently in Isabelle/Scala; removed dead code;

clarified valid_id: always standardize towards static command.id;

prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;

unused;

more uniform Execution.fork vs. Execution.print; asynchronous Execution.fork_prints, entrusted to Execution.fork management (NB: Command.print_finished is only relevant for persistent print functions);

added Execution.print: accumulate print operations for some command execution, which are applied later and print time; misc tuning;

tuned proofs

Some useful lemmas

tuned comments;

tuned load order;

superseded by (provide_)parse_files;

tuned;

merged

more warnings for recent versions of Poly/ML (see also fe1f6a1707f7);

eliminated dead code;

proper configuration option "ML_print_depth"; proper ML_exception_trace for HOL-TPTP;

removed junk;

clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);

separate tokenization and language context for SML: no symbols, no antiquotes;

separate "sml" mode, suppress old "ml" mode altogether;

some SML examples;

added command 'SML_file' for Standard ML without Isabelle/ML add-ons;

updated to scala-2.10.4;

cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)

prove theorems with fixed variables (export afterwards)

generalized theorems about derivatives of limits of sequences of funtions

removed unused 'ax_specification', to give 'specification' a chance to become localized; tuned whitespace;

merged;

merged

proper Sign.full_name to get internal name (like Sign.add_consts);

formal check of user input, avoiding direct references of interal names;

discontinued Toplevel.debug in favour of system option "exception_trace";

tuned proofs

made tactic more robust

inline helper function

rearranging some deriv theorems

modernized approximation, avoiding bad name binding;

more sensible treatment of quasi-local variables (NB: Variable.add_fixes is only for term variables, while Variable.declare takes care of types within given terms);

merged

more antiquotations;

more antiquotations;

more antiquotations; clarified file location;

more antiquotations;

more antiquotations;

more antiquotations;

tuned message;

more antiquotations;

avoid hard-wired theory names;

generalized and strengthened cong rules on compound operators, similar to 1ed737a98198

added splash screen for jvm boot, which is important for initial encounter to avoid multiple copies running against each other;

merged

more qualified names;

more qualified names;

more qualified names;

tuned;

more qualified names;