explicit indication of outer syntax with no tokens; uniform Isabelle.markers, based on syntax specification -- no tokens for NEWS;

clarified module location;

always use extended styles (despite de26cf3191a3);

more uniform configuration of editor modes and token markers;

syntax for isabelle-news with symbol completion;

tuned signature;

maintain Completion_Popup.Text_Area as client property like Document_View; global Completion_Popup.Text_Area init/exit like SideKickPlugin; eliminated old SideKick completion -- cover all Isabelle modes uniformly; dynamic lookup of Isabelle.mode_syntax -- NB: buffer mode might be undefined in intermediate stages;

some completion options;

more abstract Completion_Popup.Text_Area; more uniform font size;

GTK+ works better due to avoidance of default list view popups;

renamed BNF axiom

merge

handle type class annotations on (co)datatype parameters gracefully

store nesting_bnfs in fp_sugar (required in "nested to mutual" reduction)

cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs

qualify BNF constants properly

qualify generated constants uniformly

rationalized bindings

rationalize message generation + added a warning

removed outdated comments

build relator term for compound type (generalized build_map)

documentation ideas

renamed an ML filed for consistency (low-level => ctor/dtor/xtor in name)

merge

more

tuned proofs;

merged

tuned proofs;

tuned proofs;

complete symbols only in backslash forms -- less intrusive editing, greater chance of finding escape sequence in text; complete words >= 3 characters only; discontinued short word abbrev "Un" (see also fdd6e68e29d9 and e38e80686ce5);

tuned signature -- no need for ooddities;

tuned -- help finding rare NPE on cold start;

tuned proofs;

uniform use of isabelle.jEdit.Popup, based on generic screen location operations;

more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X); observe !evt.isConsumed semantically: no initial dismiss here (e.g. due to cursor keys);

tuned;

dismiss popups more uniformly;

more uniform check (see JEdit_Lib.propagate_key);

tuned signature;

more symbols;

tuned proofs;

tuned proofs;

tuned proofs;

enable jEdit KeyEventWorkaround uniformly;

de-register completion first, which is important to make new popup reliably;

register single instance within root, in order to get rid of old popup as user continues typing;

more careful refocus operation: do not reset focus if it was already lost (relevant when activating a different GUI component, for example);

some actual completion via outer syntax; disable old SideKick completion for "isabelle" mode;

tuned signature;

avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus; uniform JEdit_Lib.propagate_key;

determine completion geometry like tooltip; just one option jedit_popup_bounds for tooltip and completion;

explicit "hidden" operation with focus management; explicit popup_font; just one option jedit_popup_font_scale for tooltip and completion;

some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;

more standard key handling according to jEdit (with workaround); clarified handling of ESCAPE (again): dismiss without second interpretation as select-none;

more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;

got rid of old error -- users who install SPASS manually are responsible for any version mismatches

tuned messages

natural component order

better error message

tuning