tuned errors -- in accordance to Scala version;

tuned errors -- in accordance to ML antiquotations;

more explicit method reports; avoid combinator parsers with observable effect -- unreliable due to backtracking (Scan.FAIL) and incremental input (Scan.MORE);

merged

tuned whitespace; tuned proofs;

tuned whitespace; modernized theory setup;

clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits; clarified asynchronous event propagation: determine buffers where they are actually accessed; tuned signature;

simplified rendering -- no need to over-emphasize "token_range";

modernized theory setup;

store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing; integrity check of SHA1 digests produced in Scala vs. ML; tuned signature;

more symbols;

more symbol abbrevs to support HOL library maintenance;

reparse only for actually changed blobs; tuned signature;

proper document blobs for initial edit, which is relevant for loading auxiliary file buffers;

more formal Document.Blobs; removed junk;

tuned output;

proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);

tuned iterator;

tuned;

tuned comment;

tuned output;

amended some slips, rolling back currently dysfunctional export minimimalisation for Scala

A bit of tidying up

added two examples

hide Lifting.invariant from a user completely

correct most general type for mutual recursion when several identical types are involved

removed bogus "error" message (it appeared during regular mode of operation)

intermediate typedef for the type of the bound (local to lfp)

merged

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;

more positions; tuned messages;

more markup;

simplify a proof due to 6c95a39348bd

new rule for making rsp theorem more readable

unregister lifting setup following the best practice of Lifting

generalised some results using type classes

More complex-related lemmas

the rules are not needed due to 1726f46d2aa8

simplify and repair proofs due to df0fda378813

rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user

Gauss.thy ported from Old_Number_Theory (unfinished)

merged

reverted c05d3e22adaf: Locale.intern is still required by AFP/Simpl;

optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);

tuned colors;

prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);

more robust registration of code equations

be consistent and produce always rep_eq with =

publish a useful function

don't be so aggresive for a public test function and raise only BAD_THM instead of ERROR

add missing attributes

Lemmas about Reals, norm, etc., and cleaner variants of existing ones

A few lemmas about summations, etc.

merged

tuned;

tuned messages -- prefer quote before Position.here, which might be just \<here>;

clarified ML language flags;

clarified painting of invisible caret, e.g. focus change due to popup;

tuned signature -- weaker type requirement;

paint completion range of active popup;

tuned messages;

clarified Token.range_of in accordance to Symbol_Pos.range; eliminated redundant Position.set_range, which is already included in Position.range;

tuned signature;

clarified interaction with dead variables in the composition of BNFs

added BNF cache (within one definition)

updated docs

optimized 'bnf_of_typ' further w.r.t. dead variables

optimization of 'bnf_of_typ' if all variables are dead

improved accounting for dead variables when naming set functions (refines d71c2737ee21)

added explicit killing

more precise error message

reuse same parser for '(co)datatype(_new)' as for 'bnf_decl'

tuned message;

tuned proofs;

tuned whitespace;

unused;

clarified semantic completion: retain kind.full_name as official item name for history; misc tuning;

try explicit semantic completion before syntax completion;

more explicit Completion.Item.range, independently of caret;

tuned whitespace;

clarified stretch_point_range wrt. UTF-16 surrogates; tuned;

tuned;

some rendering of completion range; tuned;

clarified completion names; tuned signature;

NEWS and documentation, including correction of long-overseen "*"

regenerated

keep only identifiers public which are explicitly requested or demanded by dependencies

explicit option for "open" code generation

tuned

more fine-grain notion of export

tuned

formal markup for public ingredients

tuned