src/Pure/PIDE/document.ML
2010-09-09 ago more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-08-31 ago moved Toplevel.run_command to Pure/PIDE/document.ML;
2010-08-30 ago tuned;
2010-08-17 ago tune;
2010-08-17 ago added functor Linear_Set, based on former adhoc structures in document.ML;
2010-08-15 ago document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
2010-08-15 ago renamed create_id to new_id;
2010-08-15 ago more explicit / functional ML version of document model;
2010-08-14 ago more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
2010-08-14 ago tuned;
2010-08-12 ago clarified "state" (accumulated data) vs. "exec" (execution that produces data);
2010-08-11 ago 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);
2010-08-05 ago simplified/refined document model: collection of named nodes, without proper dependencies yet;