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;

another sample found by Stefan Berghofer;

added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;

allow NUL characters in ML string passed to C library;

simplify code (now that ctr_sugar uses the same type variables as fp_sugar)

merged

prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);

prefer Binding.name_of over Binding.print -- the latter leads to funny quotes and markup within the constructed term;

always transfer thm where attributes are applied -- relevant for internal 'notes' (e.g. via bundle 'includes') in contrast to external 'notes' (cf. Proof_Context.retrieve_thms);

proper context;

tuned

moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)

export one more ML function, needed for primcorec

reverted 6c5e7143e1f6; took a better look at evaluation data this time

tuned unchecked ML;

removed junk;

ignore trailing primes, e.g. rename \<alpha>' to \<alpha>'' instead of \<alpha>'a;

tuned fudge factor in light of evaluation

tuned proofs;

tuned proofs;

discontinued rendering of obsolete \<onesuperior>, \<twosuperior>, \<threesuperior>;

tuned;

maintain goal forks as part of global execution; tuned;

tuned proofs -- fewer warnings;

simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML); clarified Task_Queue.group_status; tuned;

discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information); simplified Goal.future_enabled;

some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1); tuned;

use view root as parent for popup, which provides more space and avoids confusion of mouse wheel handlers on Windows (wrt. text area scrollbar);

tuned proofs;

tuned proofs;

confine popup to parent component, to avoid javax.swing.PopupFactory$HeavyWeightPopup and its problems with Linux window management and Mac OS X key handling;

strict checking of coordinates wrt. inner painter component;

more static values;