| 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
|