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;

Document.print_id;

consider command state as part of Snapshot, not Document;

represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);

Named_Target;

modernized specifications; tuned headers;

spelling;

merged

renamed Theory_Target to the more appropriate Named_Target

discontinue old implementation of `foundation`

moved instantiation target formally to class_target.ML

NEWS

merged

print fcomp combinator only monadic in connection with other monadic expressions