2010-08-15 ago wenzelm document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
2010-08-15 ago wenzelm use Synchronized.var and prevent global CRITICAL sections in this hot spot;
2010-08-15 ago wenzelm renamed create_id to new_id;
2010-08-15 ago wenzelm more explicit / functional ML version of document model;
2010-08-15 ago wenzelm renamed class Document to Document.Version etc.;
2010-08-15 ago wenzelm fixed Isabelle/Scala build (cf. f3220ef79d51);
2010-08-14 ago wenzelm Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;
2010-08-14 ago wenzelm more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
2010-08-14 ago wenzelm Keyword.status: always suppress position;
2010-08-14 ago wenzelm moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
2010-08-14 ago wenzelm merged
2010-08-13 ago haftmann robustified proof
2010-08-13 ago haftmann lemma execute_bind_case
2010-08-13 ago haftmann unit and bool are instances of heap
2010-08-13 ago haftmann merged
2010-08-13 ago haftmann sketch of new outline
2010-08-13 ago haftmann sketch of new outline
2010-08-13 ago haftmann ditem
2010-08-13 ago haftmann refined abstract
2010-08-13 ago haftmann added stub "If something utterly fails"
2010-08-13 ago haftmann avoid variable name acc (cf. cs. 3142c1e21a0e)
2010-08-13 ago haftmann import swap prevents strange failure of SML code generator for datatypes
2010-08-13 ago haftmann added setup
2010-08-12 ago haftmann merged
2010-08-12 ago haftmann group record-related ML files
2010-08-12 ago haftmann merged
2010-08-12 ago haftmann dropped dead code
2010-08-12 ago haftmann moved Record.thy from session Plain to Main; avoid variable name acc
2010-08-12 ago haftmann group record-related ML files
2010-08-12 ago haftmann Class.declare -> Class.const
2010-08-12 ago haftmann named target is optional; explicit Name_Target.reinit
2010-08-12 ago haftmann named target is optional
2010-08-12 ago haftmann Named_Target.init: empty string represents theory target
2010-08-12 ago haftmann Named_Target.theory_init
2010-08-12 ago Christian Urban simplified code
2010-08-12 ago haftmann tuned
2010-08-12 ago haftmann tuned
2010-08-11 ago haftmann merged
2010-08-11 ago haftmann tuned whitespace
2010-08-11 ago haftmann tuned internal structure
2010-08-11 ago haftmann remove reinit operation alltogether
2010-08-11 ago haftmann avoid arcane Local_Theory.reinit entirely
2010-08-11 ago haftmann more convenient split of class modules: class and class_declaration
2010-08-11 ago haftmann tuned
2010-08-11 ago haftmann stripped signature
2010-08-11 ago haftmann explicit accessed to structure Class_Target
2010-08-11 ago haftmann tuned lowercase
2010-08-14 ago wenzelm moved Document.text_edits to Thy_Syntax;
2010-08-14 ago wenzelm tuned;
2010-08-13 ago wenzelm 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 ago wenzelm do not buffer fifo streams here -- done in Isabelle_Process;
2010-08-13 ago wenzelm explicit Document.State value, instead of individual state variables in Session, Command, Document;
2010-08-13 ago wenzelm edit_document: more precise status position;
2010-08-13 ago wenzelm added get_after convenience;
2010-08-12 ago wenzelm more basic notion of unparsed input;
2010-08-12 ago wenzelm simplified/clarified Change: transition prev --edits--> result, based on futures;
2010-08-12 ago wenzelm moved snapshot to Session (cf. 96b22dfeb56a);
2010-08-12 ago wenzelm Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway;
2010-08-12 ago wenzelm clarified "state" (accumulated data) vs. "exec" (execution that produces data);
2010-08-12 ago wenzelm misc tuning and simplification;