2011-08-13 wenzelm 2011-08-13 clarified node header -- exclude master_dir;
2011-08-13 wenzelm 2011-08-13 maintain node header; misc tuning and clarification;
2011-08-12 wenzelm 2011-08-12 clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
2011-08-11 wenzelm 2011-08-11 uniform treatment of header edits as document edits;
2011-08-11 wenzelm 2011-08-11 explicit datatypes for document node edits;
2011-07-10 wenzelm 2011-07-10 propagate header changes to prover process; simplified Document case classes; Document.State.assignments: indexed by Version_ID;
2011-07-09 wenzelm 2011-07-09 some support for blobs (arbitrary text files) within document nodes;
2011-07-07 wenzelm 2011-07-07 explicit Document.Node.Header, with master_dir and thy_name; imitate ML path operations more closely;
2011-07-04 wenzelm 2011-07-04 Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
2011-07-04 wenzelm 2011-07-04 explicit class Counter;
2011-07-03 wenzelm 2011-07-03 tuned signature;
2010-11-28 wenzelm 2010-11-28 tuned signature;
2010-11-11 wenzelm 2010-11-11 unified type Document.Edit;
2010-11-11 wenzelm 2010-11-11 replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes; Document_Model.pending_edits: more robust treatment of init, including buffer reload event (jEdit 4.3.2 produces malformed remove/insert that lacks the last character); tuned;
2010-11-10 wenzelm 2010-11-10 proper treatment of equal heading level;
2010-11-10 wenzelm 2010-11-10 some support for nested source structure, based on section headings;
2010-08-30 wenzelm 2010-08-30 text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;
2010-08-20 wenzelm 2010-08-20 tuned signatures;
2010-08-15 wenzelm 2010-08-15 moved Text_Edit to Text.Edit; tuned;
2010-08-15 wenzelm 2010-08-15 renamed create_id to new_id;
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-14 wenzelm 2010-08-14 moved Document.text_edits to Thy_Syntax;
2010-08-14 wenzelm 2010-08-14 tuned;
2010-08-08 wenzelm 2010-08-08 parse_spans: somewhat faster low-level implementation;
2010-05-17 wenzelm 2010-05-17 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
2010-05-15 wenzelm 2010-05-15 renamed Outer_Parse to Parse (in Scala);
2010-01-11 wenzelm 2010-01-11 Outer_Lex.is_ignored;
2010-01-10 wenzelm 2010-01-10 plain object;
2010-01-05 wenzelm 2010-01-05 separate module Thy_Syntax for command span parsing;