2010-01-11 wenzelm 2010-01-11 more timing;
2010-01-11 wenzelm 2010-01-11 more tobust treatment of Document.current_state; some timing;
2010-01-11 wenzelm 2010-01-11 new unparsed span for text right after existing command; tuned;
2010-01-11 wenzelm 2010-01-11 eliminated strange mutable var commands; removed_commands: refer to old commands; misc tuning;
2010-01-11 wenzelm 2010-01-11 updated header;
2010-01-11 wenzelm 2010-01-11 do not override Command.hashCode -- which was inconsistent with eq anyway; unparsed: no id, commands observe pointer equality; actually invoke edit_commands; more correct doc_edits; tuned;
2010-01-11 wenzelm 2010-01-11 renamed Command.content to source; reorganization of document parsing, using command spans etc. -- initial setup;
2010-01-10 wenzelm 2010-01-10 iterators for ranges of commands/starts -- avoid extra array per document; try/finally for saved_color; misc tuning;
2010-01-10 wenzelm 2010-01-10 misc tuning and clarification of Document/Change;
2010-01-06 wenzelm 2010-01-06 more precise treatment of document/state assigment;
2010-01-05 wenzelm 2010-01-05 use Text_Edit provided by Isabelle;
2010-01-04 wenzelm 2010-01-04 back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states; recent_document: require finished state assignment; explicitly typed Session.lookup_command;
2010-01-03 wenzelm 2010-01-03 more explicit treatment of command/document state; misc tuning and clarification;
2010-01-01 wenzelm 2010-01-01 eliminated redundant session documents database; tuned;
2010-01-01 wenzelm 2010-01-01 use isabelle.Future; tuned;
2010-01-01 wenzelm 2010-01-01 renamed current_document to recent_document (might be a bit older than current_change); Change: explicit future value of Document.Change instead of implicit lookup in Session database; Document_Model: apply Document.text_edits here (as future);
2010-01-01 wenzelm 2010-01-01 renamed Proof_Document to Document;