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