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