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

merged

merged

moved overloading target formally to overloading.ML

moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order

merged

whitespace tuning