tuned specifications and proofs;

more precise before_caret_range (looking both in space and time);

improved rendering of blinking cursor;

markup for method combinators;

tuned;

tuned signature;

suppress completion of obscure keyword, avoid confusion with plain "simp";

method language markup, e.g. relevant to prevent outer keyword completion;

transfer domain rule for special case of functions - was missing

replaced smt-based proof with metis proof that requires no external tool

obsolete workaround

prefer proof context over background theory

made tactics more robust

merged

tuned specifications and proofs;

merged

uniform insert vs. popup policy;

tuned proofs;

back to Markup.command for actual tokens (amending 4a4e5686e091) -- avoid conflict of jEdit token marker with Rendering.text_colors;

tuned signature;

no word completion within word context;

more completion rendering: active, semantic, syntactic; tuned;

tuned;

tuned message -- more markup;

clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind; tuned message;

proper context for global data;

modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion; removed obsolete Method.Source_i; proper context for global data; tuned messages;

optimize special case according to Library.merge (see also 8fbc355100f2); no treatment for Net.merge, due to non-standard merge order;