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

tuned

use only one data slot; rename print_quotmaps to print_quot_maps; tuned

merged

added rtrancl_while

renamed inner_dense_linorder to dense_linorder

renamed typeclass dense_linorder to unbounded_dense_linorder

tuned imports; tuned proofs;