document value generation for quickcheck's testers

tuned whitespace;

suppress slightly odd completion of "simp";

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;