prefer abstract datatype -- in accordance to ML version;

tuned data structure;

tuned;

tuned comment;

tuned signature;

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