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

remove overloading and instantiation from data slot

removed obsolete Toplevel.enter_proof_body;

standardized pretty printing of consts (e.g. see find_theorems, print_theory);

misc tuning and simplification;

simplified/unified command setup;