| Wed, 03 Dec 2014 22:34:28 +0100 |
wenzelm |
node-specific keywords, with session base syntax as default;
|
file |
diff |
annotate
|
| Tue, 02 Dec 2014 14:16:56 +0100 |
wenzelm |
node-specific syntax, with base_syntax as default;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 00:17:02 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 00:08:32 +0200 |
wenzelm |
separate module Command_Span: mostly syntactic representation;
|
file |
diff |
annotate
|
| Mon, 11 Aug 2014 22:59:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 11 Aug 2014 22:43:26 +0200 |
wenzelm |
tuned output, in accordance to transaction name in ML;
|
file |
diff |
annotate
|
| Mon, 11 Aug 2014 22:29:48 +0200 |
wenzelm |
more explicit type Span in Scala, according to ML version;
|
file |
diff |
annotate
|
| Mon, 11 Aug 2014 20:46:56 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 02 Aug 2014 16:35:59 +0200 |
wenzelm |
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 21:01:28 +0200 |
wenzelm |
more frugal edits;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 20:03:00 +0200 |
wenzelm |
simplified Text.Chunk -- eliminated ooddities;
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 21:08:00 +0200 |
wenzelm |
clarified Version.syntax -- avoid guessing initial situation;
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 20:53:35 +0200 |
wenzelm |
more abstract Prover.Syntax, as proposed by Carst Tankink;
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 20:41:44 +0200 |
wenzelm |
tuned signature -- more explicit iterator terminology;
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 20:22:12 +0200 |
wenzelm |
more explicit iterator terminology, in accordance to Scala 2.8 library;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 15:28:14 +0200 |
wenzelm |
tuned signature -- more static typing;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 15:05:24 +0200 |
wenzelm |
store blob content within document node: aux. files that were once open are made persistent;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2014 10:49:32 +0100 |
wenzelm |
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
|
file |
diff |
annotate
|
| Sat, 29 Mar 2014 10:17:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2014 09:34:51 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 17:39:03 +0100 |
wenzelm |
clarifed module name;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 14:51:14 +0100 |
wenzelm |
reparse only for actually changed blobs;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 14:07:04 +0100 |
wenzelm |
more formal Document.Blobs;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 10:58:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 11:28:17 +0100 |
wenzelm |
maintain blob edits within history, which is important for Snapshot.convert/revert;
|
file |
diff |
annotate
|
| Tue, 11 Feb 2014 17:44:29 +0100 |
wenzelm |
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 15:29:40 +0100 |
wenzelm |
propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
|
file |
diff |
annotate
|
| Wed, 22 Jan 2014 21:33:50 +0100 |
wenzelm |
clarified approximative syntax of thy_load commands: first name after command keyword, after cleaning wrt. tags and cmts;
|
file |
diff |
annotate
|
| Fri, 22 Nov 2013 21:13:44 +0100 |
wenzelm |
clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 22:12:54 +0100 |
wenzelm |
more explicit indication of missing files;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 20:53:43 +0100 |
wenzelm |
clarified Document.Blobs environment vs. actual edits of auxiliary files;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 19:33:27 +0100 |
wenzelm |
maintain blobs within document state: digest + text in ML, digest-only in Scala;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 13:54:02 +0100 |
wenzelm |
always reparse nodes with thy_load commands, to update inlined files;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 13:39:12 +0100 |
wenzelm |
proper Thy_Load.append of auxiliary file names;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 12:57:56 +0100 |
wenzelm |
clarified boundary cases of Document.Node.Name;
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 23:26:15 +0100 |
wenzelm |
inline blobs into command, via SHA1 digest;
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 17:16:56 +0100 |
wenzelm |
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
|
file |
diff |
annotate
|
| Sun, 17 Nov 2013 17:22:55 +0100 |
wenzelm |
explicit indication of thy_load commands;
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 16:06:12 +0200 |
wenzelm |
clarified command spans (again, see also 03a2dc9e0624): restrict to proper range to allow Isabelle.command_edit adding material monotonically without destroying the command (e.g. relevant for sendback from sledgehammer);
|
file |
diff |
annotate
|
| Wed, 07 Aug 2013 20:32:54 +0200 |
wenzelm |
maintain commands together with index -- avoid redundant reconstruction of full_index;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2013 11:44:17 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 15:03:52 +0200 |
wenzelm |
commands with overlay remain visible, to avoid loosing printed output;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2013 14:26:09 +0200 |
wenzelm |
maintain overlays within node perspective;
|
file |
diff |
annotate
|
| Wed, 31 Jul 2013 12:14:13 +0200 |
wenzelm |
allow explicit indication of required node: full eval, no prints;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 22:09:16 +0200 |
wenzelm |
tuned signature -- eliminated pointless type synonym;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 15:38:03 +0200 |
wenzelm |
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
|
file |
diff |
annotate
|
| Sun, 06 Jan 2013 14:11:15 +0100 |
wenzelm |
export some generally useful operations;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 17:29:23 +0100 |
wenzelm |
more careful handling of Dialog_Result, with active area and color feedback;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 14:41:41 +0200 |
wenzelm |
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 13:18:45 +0200 |
wenzelm |
some support for inital command markup;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 16:56:18 +0200 |
wenzelm |
more direct cumulation of (sparse) keywords;
|
file |
diff |
annotate
|
| Fri, 10 Aug 2012 15:14:45 +0200 |
wenzelm |
apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
|
file |
diff |
annotate
|
| Fri, 10 Aug 2012 13:33:07 +0200 |
wenzelm |
clarified undefined, unparsed, unfinished command spans;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2012 21:09:24 +0200 |
wenzelm |
refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2012 19:51:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2012 19:37:42 +0200 |
wenzelm |
more direct Linear_Set.reverse, swapping orientation of the graph;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 22:25:17 +0200 |
wenzelm |
more structural parsing for minor modes;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 15:01:48 +0200 |
wenzelm |
simplified Document.Node.Header -- internalized errors;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 13:21:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 24 May 2012 17:05:30 +0200 |
wenzelm |
reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy");
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 11:49:08 +0200 |
wenzelm |
discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 14:59:31 +0100 |
wenzelm |
clarified command span classification: strict Command.is_command, permissive Command.name;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 21:20:23 +0100 |
wenzelm |
more abstract heading level;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 17:45:54 +0100 |
wenzelm |
more explicit header_edits before main text_edits;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 14:13:49 +0100 |
wenzelm |
basic support for outer syntax keywords in theory header;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 11:37:56 +0100 |
wenzelm |
maintain Version.syntax within document state;
|
file |
diff |
annotate
|
| Sun, 04 Mar 2012 16:02:14 +0100 |
wenzelm |
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 |
wenzelm |
proper update_header;
|
file |
diff |
annotate
|
| Wed, 29 Feb 2012 23:09:06 +0100 |
wenzelm |
clarified module Thy_Load;
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 17:44:09 +0100 |
wenzelm |
more abstract class Document.Version;
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 17:15:33 +0100 |
wenzelm |
more abstract class Document.Node;
|
file |
diff |
annotate
|
| Sat, 26 Nov 2011 17:10:03 +0100 |
wenzelm |
sharing of token source with span source;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 13:34:45 +0200 |
wenzelm |
more abstract Document.Node.Name;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 15:41:22 +0200 |
wenzelm |
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 |
wenzelm |
slightly more abstract Command.Perspective;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 11:27:37 +0200 |
wenzelm |
slightly more abstract Text.Perspective;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 16:49:48 +0200 |
wenzelm |
clarified Document.Node.clear -- retain header (cf. ML version);
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 13:03:39 +0200 |
wenzelm |
update_perspective without actual edits, bypassing the full state assignment protocol;
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 16:41:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 12:20:12 +0200 |
wenzelm |
propagate editor perspective through document model;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 20:20:36 +0200 |
wenzelm |
provide node header via Scala layer;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 15:59:26 +0200 |
wenzelm |
clarified node header -- exclude master_dir;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 13:42:35 +0200 |
wenzelm |
maintain node header;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2011 15:28:30 +0200 |
wenzelm |
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 |
wenzelm |
uniform treatment of header edits as document edits;
|
file |
diff |
annotate
|
| Thu, 11 Aug 2011 18:01:28 +0200 |
wenzelm |
explicit datatypes for document node edits;
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 00:21:19 +0200 |
wenzelm |
propagate header changes to prover process;
|
file |
diff |
annotate
|
| Sat, 09 Jul 2011 13:29:33 +0200 |
wenzelm |
some support for blobs (arbitrary text files) within document nodes;
|
file |
diff |
annotate
|
| Thu, 07 Jul 2011 22:04:30 +0200 |
wenzelm |
explicit Document.Node.Header, with master_dir and thy_name;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2011 22:25:33 +0200 |
wenzelm |
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 |
wenzelm |
explicit class Counter;
|
file |
diff |
annotate
|
| Sun, 03 Jul 2011 15:10:17 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 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
|