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

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;