renamed class Document to Document.Version etc.; renamed Change.prev to Change.previous, and Change.document to Change.current; tuned;

fixed Isabelle/Scala build (cf. f3220ef79d51);

Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;

more basic Markup.parse_int/print_int (using signed_string_of_int) (ML); added convenient Markup.Int/Long objects (Scala); simplified "assign" message format -- explicit version id; misc tuning and simplification;

Keyword.status: always suppress position;

moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;

merged

robustified proof

lemma execute_bind_case

unit and bool are instances of heap

merged

sketch of new outline

sketch of new outline

ditem

refined abstract

added stub "If something utterly fails"

avoid variable name acc (cf. cs. 3142c1e21a0e)

import swap prevents strange failure of SML code generator for datatypes

added setup

merged

group record-related ML files

merged

dropped dead code

moved Record.thy from session Plain to Main; avoid variable name acc

group record-related ML files

Class.declare -> Class.const

named target is optional; explicit Name_Target.reinit

named target is optional

Named_Target.init: empty string represents theory target

Named_Target.theory_init

simplified code

tuned

tuned

merged

tuned whitespace

tuned internal structure

remove reinit operation alltogether

avoid arcane Local_Theory.reinit entirely

more convenient split of class modules: class and class_declaration

tuned

stripped signature

explicit accessed to structure Class_Target

tuned lowercase

moved Document.text_edits to Thy_Syntax;

tuned;

added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);

do not buffer fifo streams here -- done in Isabelle_Process; removed misleading comments -- blocking on open is not reliable on non-standard systems (Cygwin);

explicit Document.State value, instead of individual state variables in Session, Command, Document; Session.snapshot: pure value based on Document.State; Document.edit_texts: no treatment of state assignment here;

edit_document: more precise status position;

added get_after convenience;

more basic notion of unparsed input;

simplified/clarified Change: transition prev --edits--> result, based on futures; Session.history: plain List instead of somewhat indirect Change.ancestors; tuned;

moved snapshot to Session (cf. 96b22dfeb56a);

Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway; Document.edit_text: create new document id here;

clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type Document.id (ML) / Document.ID;

misc tuning and simplification;

specific command state;

specific Session.Commands_Changed;

consider snapshot as service of Session, not Document.Change;

tuned scope;