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;