wenzelm [Thu, 05 Aug 2010 21:40:20 +0200] rev 38155
editor mode;
wenzelm [Thu, 05 Aug 2010 18:17:59 +0200] rev 38154
Text_Edit.convert/revert;
wenzelm [Thu, 05 Aug 2010 18:13:12 +0200] rev 38153
renamed to_current to convert, and from_current to revert;
wenzelm [Thu, 05 Aug 2010 18:00:37 +0200] rev 38152
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm [Thu, 05 Aug 2010 16:58:18 +0200] rev 38151
explicit Change.Snapshot and Document.Node;
misc tuning and clarification;
Document_View: explicitly highlight outdated command status;
wenzelm [Thu, 05 Aug 2010 14:35:35 +0200] rev 38150
simplified/refined document model: collection of named nodes, without proper dependencies yet;
moved basic type definitions for ids and edits from Isar_Document to Document;
removed begin_document/end_document for now -- nodes emerge via edits;
edits refer to named nodes explicitly;
wenzelm [Thu, 05 Aug 2010 13:41:00 +0200] rev 38149
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm [Wed, 04 Aug 2010 16:28:45 +0200] rev 38148
uniform naming of imports (source specification) vs. parents (thy node names) vs. parent_thys (theory values);
wenzelm [Wed, 04 Aug 2010 16:11:51 +0200] rev 38147
load_thy/after_load: explicit check of parent theories, which might have failed to join proofs -- avoid uninformative crash via Graph.UNDEF;
wenzelm [Wed, 04 Aug 2010 15:50:55 +0200] rev 38146
export use_thys_wrt;