2010-08-15 wenzelm 2010-08-15 renamed class Document to Document.Version etc.; renamed Change.prev to Change.previous, and Change.document to Change.current; tuned;
2010-08-15 wenzelm 2010-08-15 fixed Isabelle/Scala build (cf. f3220ef79d51);
2010-08-14 wenzelm 2010-08-14 Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;
2010-08-14 wenzelm 2010-08-14 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML); added convenient Markup.Int/Long objects (Scala); simplified "assign" message format -- explicit version id; misc tuning and simplification;
2010-08-14 wenzelm 2010-08-14 Keyword.status: always suppress position;
2010-08-14 wenzelm 2010-08-14 moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
2010-08-14 wenzelm 2010-08-14 merged
2010-08-13 haftmann 2010-08-13 robustified proof
2010-08-13 haftmann 2010-08-13 lemma execute_bind_case
2010-08-13 haftmann 2010-08-13 unit and bool are instances of heap
2010-08-13 haftmann 2010-08-13 merged
2010-08-13 haftmann 2010-08-13 sketch of new outline
2010-08-13 haftmann 2010-08-13 sketch of new outline
2010-08-13 haftmann 2010-08-13 ditem
2010-08-13 haftmann 2010-08-13 refined abstract
2010-08-13 haftmann 2010-08-13 added stub "If something utterly fails"
2010-08-13 haftmann 2010-08-13 avoid variable name acc (cf. cs. 3142c1e21a0e)
2010-08-13 haftmann 2010-08-13 import swap prevents strange failure of SML code generator for datatypes
2010-08-13 haftmann 2010-08-13 added setup
2010-08-12 haftmann 2010-08-12 merged
2010-08-12 haftmann 2010-08-12 group record-related ML files
2010-08-12 haftmann 2010-08-12 merged
2010-08-12 haftmann 2010-08-12 dropped dead code
2010-08-12 haftmann 2010-08-12 moved Record.thy from session Plain to Main; avoid variable name acc
2010-08-12 haftmann 2010-08-12 group record-related ML files
2010-08-12 haftmann 2010-08-12 Class.declare -> Class.const
2010-08-12 haftmann 2010-08-12 named target is optional; explicit Name_Target.reinit
2010-08-12 haftmann 2010-08-12 named target is optional
2010-08-12 haftmann 2010-08-12 Named_Target.init: empty string represents theory target
2010-08-12 haftmann 2010-08-12 Named_Target.theory_init
2010-08-12 Christian Urban 2010-08-12 simplified code
2010-08-12 haftmann 2010-08-12 tuned
2010-08-12 haftmann 2010-08-12 tuned
2010-08-11 haftmann 2010-08-11 merged
2010-08-11 haftmann 2010-08-11 tuned whitespace
2010-08-11 haftmann 2010-08-11 tuned internal structure
2010-08-11 haftmann 2010-08-11 remove reinit operation alltogether
2010-08-11 haftmann 2010-08-11 avoid arcane Local_Theory.reinit entirely
2010-08-11 haftmann 2010-08-11 more convenient split of class modules: class and class_declaration
2010-08-11 haftmann 2010-08-11 tuned
2010-08-11 haftmann 2010-08-11 stripped signature
2010-08-11 haftmann 2010-08-11 explicit accessed to structure Class_Target
2010-08-11 haftmann 2010-08-11 tuned lowercase
2010-08-14 wenzelm 2010-08-14 moved Document.text_edits to Thy_Syntax;
2010-08-14 wenzelm 2010-08-14 tuned;
2010-08-13 wenzelm 2010-08-13 added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);
2010-08-13 wenzelm 2010-08-13 do not buffer fifo streams here -- done in Isabelle_Process; removed misleading comments -- blocking on open is not reliable on non-standard systems (Cygwin);
2010-08-13 wenzelm 2010-08-13 explicit Document.State value, instead of individual state variables in Session, Command, Document; Session.snapshot: pure value based on Document.State; Document.edit_texts: no treatment of state assignment here;
2010-08-13 wenzelm 2010-08-13 edit_document: more precise status position;
2010-08-13 wenzelm 2010-08-13 added get_after convenience;
2010-08-12 wenzelm 2010-08-12 more basic notion of unparsed input;
2010-08-12 wenzelm 2010-08-12 simplified/clarified Change: transition prev --edits--> result, based on futures; Session.history: plain List instead of somewhat indirect Change.ancestors; tuned;
2010-08-12 wenzelm 2010-08-12 moved snapshot to Session (cf. 96b22dfeb56a);
2010-08-12 wenzelm 2010-08-12 Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway; Document.edit_text: create new document id here;
2010-08-12 wenzelm 2010-08-12 clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type Document.id (ML) / Document.ID;
2010-08-12 wenzelm 2010-08-12 misc tuning and simplification;
2010-08-12 wenzelm 2010-08-12 specific command state;
2010-08-12 wenzelm 2010-08-12 specific Session.Commands_Changed;
2010-08-12 wenzelm 2010-08-12 consider snapshot as service of Session, not Document.Change;
2010-08-12 wenzelm 2010-08-12 tuned scope;