src/Pure/Isar/isar_document.ML
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-29 ago define_state/new_state: provide state immediately, which is now lazy;
2010-05-27 ago substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up;
2010-05-27 ago further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;
2010-05-15 ago renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 ago renamed structure ValueParse to Parse_Value;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-01-06 ago always report updates -- required has "handshake";
2010-01-04 ago explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);
2009-12-30 ago eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id;
2009-12-29 ago back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
2009-12-29 ago removed slightly odd Isar_Document.init;
2009-10-27 ago non-critical atomic accesses;
2009-09-30 ago actually perform Isar_Document.init on startup;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-09-15 ago Isar.define_command: identify transaction;
2009-09-01 ago modernized Isar_Document;
2009-06-04 ago uniform (short) ids on both sides;
2009-01-16 ago define_state: use empty_state;
2009-01-16 ago provide end_document;
2009-01-16 ago run command: check theory name for init;
2009-01-16 ago fold_entries: non-optional start, permissive;
2009-01-15 ago command 'Isar.edit_document': actually invoke edit_document;
2009-01-15 ago tuned;
2009-01-15 ago edit_document: proper edits/edit markup, including the document id;
2009-01-15 ago removed junk;
2009-01-15 ago misc cleanup and simplification;
2009-01-13 ago misc internal rearrangements;
2009-01-13 ago replaced sys_error by plain error;
2009-01-13 ago added Isar/isar_document.ML: Interactive Isar documents.