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;