| Thu, 15 Mar 2012 17:45:54 +0100 |
more explicit header_edits before main text_edits;
|
file | diff | annotate |
| Thu, 15 Mar 2012 14:13:49 +0100 |
basic support for outer syntax keywords in theory header;
|
file | diff | annotate |
| Thu, 15 Mar 2012 11:37:56 +0100 |
maintain Version.syntax within document state;
|
file | diff | annotate |
| Sun, 04 Mar 2012 16:02:14 +0100 |
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
|
file | diff | annotate |
| Thu, 01 Mar 2012 15:42:44 +0100 |
proper update_header;
|
file | diff | annotate |
| Wed, 29 Feb 2012 23:09:06 +0100 |
clarified module Thy_Load;
|
file | diff | annotate |
| Sun, 26 Feb 2012 17:44:09 +0100 |
more abstract class Document.Version;
|
file | diff | annotate |
| Sun, 26 Feb 2012 17:15:33 +0100 |
more abstract class Document.Node;
|
file | diff | annotate |
| Sat, 26 Nov 2011 17:10:03 +0100 |
sharing of token source with span source;
|
file | diff | annotate |
| Thu, 01 Sep 2011 13:34:45 +0200 |
more abstract Document.Node.Name;
|
file | diff | annotate |
| Wed, 31 Aug 2011 15:41:22 +0200 |
maintain name of *the* enclosing node as part of command -- avoid full document traversal;
|
file | diff | annotate |
| Thu, 25 Aug 2011 11:41:48 +0200 |
slightly more abstract Command.Perspective;
|
file | diff | annotate |
| Thu, 25 Aug 2011 11:27:37 +0200 |
slightly more abstract Text.Perspective;
|
file | diff | annotate |
| Wed, 24 Aug 2011 16:49:48 +0200 |
clarified Document.Node.clear -- retain header (cf. ML version);
|
file | diff | annotate |
| Wed, 24 Aug 2011 13:03:39 +0200 |
update_perspective without actual edits, bypassing the full state assignment protocol;
|
file | diff | annotate |
| Tue, 23 Aug 2011 16:41:16 +0200 |
tuned signature;
|
file | diff | annotate |
| Tue, 23 Aug 2011 12:20:12 +0200 |
propagate editor perspective through document model;
|
file | diff | annotate |
| Sat, 13 Aug 2011 20:20:36 +0200 |
provide node header via Scala layer;
|
file | diff | annotate |
| Sat, 13 Aug 2011 15:59:26 +0200 |
clarified node header -- exclude master_dir;
|
file | diff | annotate |
| Sat, 13 Aug 2011 13:42:35 +0200 |
maintain node header;
|
file | diff | annotate |
| Fri, 12 Aug 2011 15:28:30 +0200 |
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
|
file | diff | annotate |
| Thu, 11 Aug 2011 20:32:44 +0200 |
uniform treatment of header edits as document edits;
|
file | diff | annotate |
| Thu, 11 Aug 2011 18:01:28 +0200 |
explicit datatypes for document node edits;
|
file | diff | annotate |
| Sun, 10 Jul 2011 00:21:19 +0200 |
propagate header changes to prover process;
|
file | diff | annotate |
| Sat, 09 Jul 2011 13:29:33 +0200 |
some support for blobs (arbitrary text files) within document nodes;
|
file | diff | annotate |
| Thu, 07 Jul 2011 22:04:30 +0200 |
explicit Document.Node.Header, with master_dir and thy_name;
|
file | diff | annotate |
| Mon, 04 Jul 2011 22:25:33 +0200 |
Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
|
file | diff | annotate |
| Mon, 04 Jul 2011 20:18:19 +0200 |
explicit class Counter;
|
file | diff | annotate |
| Sun, 03 Jul 2011 15:10:17 +0200 |
tuned signature;
|
file | diff | annotate |
| Sun, 28 Nov 2010 19:35:14 +0100 |
tuned signature;
|
file | diff | annotate |
| Thu, 11 Nov 2010 17:07:05 +0100 |
unified type Document.Edit;
|
file | diff | annotate |
| Thu, 11 Nov 2010 16:48:46 +0100 |
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 |
proper treatment of equal heading level;
|
file | diff | annotate |
| Wed, 10 Nov 2010 15:00:40 +0100 |
some support for nested source structure, based on section headings;
|
file | diff | annotate |
| Mon, 30 Aug 2010 20:12:43 +0200 |
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 |
tuned signatures;
|
file | diff | annotate |
| Sun, 15 Aug 2010 21:42:13 +0200 |
moved Text_Edit to Text.Edit;
|
file | diff | annotate |
| Sun, 15 Aug 2010 19:30:11 +0200 |
renamed create_id to new_id;
|
file | diff | annotate |
| Sun, 15 Aug 2010 14:18:52 +0200 |
renamed class Document to Document.Version etc.;
|
file | diff | annotate |
| Sat, 14 Aug 2010 12:01:50 +0200 |
moved Document.text_edits to Thy_Syntax;
|
file | diff | annotate |
| Sat, 14 Aug 2010 11:52:24 +0200 |
tuned;
|
file | diff | annotate |
| Sun, 08 Aug 2010 22:33:41 +0200 |
parse_spans: somewhat faster low-level implementation;
|
file | diff | annotate |
| Mon, 17 May 2010 14:23:54 +0200 |
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
|
file | diff | annotate |
| Sat, 15 May 2010 22:15:57 +0200 |
renamed Outer_Parse to Parse (in Scala);
|
file | diff | annotate |
| Mon, 11 Jan 2010 18:23:06 +0100 |
Outer_Lex.is_ignored;
|
file | diff | annotate |
| Sun, 10 Jan 2010 23:16:26 +0100 |
plain object;
|
file | diff | annotate |
| Tue, 05 Jan 2010 16:29:31 +0100 |
separate module Thy_Syntax for command span parsing;
|
file | diff | annotate |