Sun, 28 Nov 2010 19:35:14 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 11 Nov 2010 17:07:05 +0100 |
wenzelm |
unified type Document.Edit;
|
file |
diff |
annotate
|
Thu, 11 Nov 2010 16:48:46 +0100 |
wenzelm |
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
|
file |
diff |
annotate
|
Wed, 10 Nov 2010 15:42:20 +0100 |
wenzelm |
proper treatment of equal heading level;
|
file |
diff |
annotate
|
Wed, 10 Nov 2010 15:00:40 +0100 |
wenzelm |
some support for nested source structure, based on section headings;
|
file |
diff |
annotate
|
Mon, 30 Aug 2010 20:12:43 +0200 |
wenzelm |
text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;
|
file |
diff |
annotate
|
Fri, 20 Aug 2010 20:11:25 +0200 |
wenzelm |
tuned signatures;
|
file |
diff |
annotate
|
Sun, 15 Aug 2010 21:42:13 +0200 |
wenzelm |
moved Text_Edit to Text.Edit;
|
file |
diff |
annotate
|
Sun, 15 Aug 2010 19:30:11 +0200 |
wenzelm |
renamed create_id to new_id;
|
file |
diff |
annotate
|
Sun, 15 Aug 2010 14:18:52 +0200 |
wenzelm |
renamed class Document to Document.Version etc.;
|
file |
diff |
annotate
|
Sat, 14 Aug 2010 12:01:50 +0200 |
wenzelm |
moved Document.text_edits to Thy_Syntax;
|
file |
diff |
annotate
|
Sat, 14 Aug 2010 11:52:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 08 Aug 2010 22:33:41 +0200 |
wenzelm |
parse_spans: somewhat faster low-level implementation;
|
file |
diff |
annotate
|
Mon, 17 May 2010 14:23:54 +0200 |
wenzelm |
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
|
file |
diff |
annotate
|
Sat, 15 May 2010 22:15:57 +0200 |
wenzelm |
renamed Outer_Parse to Parse (in Scala);
|
file |
diff |
annotate
|
Mon, 11 Jan 2010 18:23:06 +0100 |
wenzelm |
Outer_Lex.is_ignored;
|
file |
diff |
annotate
|
Sun, 10 Jan 2010 23:16:26 +0100 |
wenzelm |
plain object;
|
file |
diff |
annotate
|
Tue, 05 Jan 2010 16:29:31 +0100 |
wenzelm |
separate module Thy_Syntax for command span parsing;
|
file |
diff |
annotate
|