back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; discontinued obsolete option jedit_completion_dismiss_delay (see 750561986828); more explicit shutdown;

remove unnecessary finiteness assumptions from lemmas about setsum

adapt to Isabelle/c726ecfb22b6

fix HOL-NSA; move lemmas

cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}

changed policy when to define constants

tuned proofs; removed duplicated facts

additional lemmas

removed dependencies on theory Ordered_Euclidean_Space

use cbox to relax class constraints

merged

tuned;

more antiquotations;

more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;

remove sums_seq, it is not used

update syntax of has_*derivative to infix 50; fixed proofs

unify syntax for has_derivative and differentiable

tuned proofs

tuned internal construction

a few new theorems

proper flags for main action (amending 638b29331549);

tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;

merge semantic and syntax completion; tuned;

tuned;

tuned signature;

tuned signature;

clarified key event propagation, in accordance to outer_key_listener;

allow implicit semantic completion, notably after delay that exceeds usual round-trip time; clarified isabelle.completion action: already open popup is re-opened and thus updated;

reject internal names, notably from Term.free_dummy_patterns;

more uniform alias vs. hide: proper check, allow to hide global names as well;

tuned proofs

normalising simp rules for compound operators

tuned markup;

minor tuning;

more markup;

clarified completion ordering: prefer local names;

tuned signature; eliminated clones;

tuned -- avoid vacuous reports;

clarified local facts;

more explicit treatment of verbose mode, which includes concealed entries;

removed dead code;

clarified retrieve_generic: local error takes precedence, which is relevant for completion;

clarified print_local_facts;

more complete set of lemmas wrt. image and composition

merge

add error messages for invalid inputs

add lemmas about nhds filter; tuned proof

remove unused lemma which was a direct consequence of tendsto_intros

merged

merged

prefer more robust Synchronized.var;

discontinued somewhat pointless "thy_script" keyword kind;

conceal improper cases, e.g. relevant for completion (and potentially for markup);

conceal somewhat obscure internal facts, e.g. relevant for 'print_theorems', 'find_theorems';

more accurate resolution of hybrid facts, which actually changes the sort order of results;

tuned -- command 'text' was localized some years ago;

back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;

just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.); more thorough background_notes: distribute global notes to all contexts;

more frugal recording of changes: join merely requires information from one side; tuned;

do not test details of error messages;