| Sat, 01 Mar 2014 12:07:26 +0100 |
wenzelm |
tuned signature -- more explicit Document.Elements;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 11:58:26 +0100 |
wenzelm |
tuned data structure;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 11:50:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 14:07:04 +0100 |
wenzelm |
more formal Document.Blobs;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 12:48:59 +0100 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 20:56:55 +0100 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 11:05:02 +0100 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 15:48:04 +0100 |
wenzelm |
tuned signature -- avoid redundancy and confusion of flags;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 15:22:06 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 15:12:50 +0100 |
wenzelm |
more general / abstract Command.Markups, with separate index for status elements;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 16:00:37 +0100 |
wenzelm |
cumulate/select wrt. precise elements guard;
|
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
|
| Wed, 12 Feb 2014 11:05:48 +0100 |
wenzelm |
more accurate eq_content;
|
file |
diff |
annotate
|
| Tue, 11 Feb 2014 21:58:31 +0100 |
wenzelm |
maintain multiple command chunks and markup trees: for main chunk and loaded files;
|
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
|
| 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
|
| Thu, 21 Nov 2013 17:50:23 +0100 |
wenzelm |
actually expose errors of cumulative theory dependencies;
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 15:53:59 +0100 |
wenzelm |
ranges of thy_load commands count as visible within perspective;
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 12:24:54 +0100 |
wenzelm |
refer to thy_load command of auxiliary file;
|
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 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:24:04 +0100 |
wenzelm |
tuned;
|
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
|
| Sat, 12 Oct 2013 00:10:07 +0200 |
wenzelm |
more strict find_command -- avoid invalid hyperlink_command;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 14:53:16 +0200 |
wenzelm |
prefer PIDE editor operations;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 14:27:58 +0200 |
wenzelm |
central management of Document.Overlays, independent of Document_Model;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 13:32:26 +0200 |
wenzelm |
tuned -- use Multi_Map;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 11:49:58 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 17:04:02 +0200 |
wenzelm |
proper low-level comparison -- heed warning by Scala compiler;
|
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 19:59:58 +0200 |
wenzelm |
more elementary list structures for markup tree traversal;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2013 13:46:32 +0200 |
wenzelm |
more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2013 11:44:17 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 15:29:10 +0200 |
wenzelm |
tuned signature -- more uniform treatment of overlays as command mapping;
|
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
|
| Tue, 09 Jul 2013 18:11:31 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 17:58:38 +0200 |
wenzelm |
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 13:24:17 +0200 |
wenzelm |
tuned signature -- NB: Command.read is actually part of Command.eval;
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 13:17:22 +0200 |
wenzelm |
tuned protocol terminology;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 16:01:45 +0200 |
wenzelm |
tuned signature;
|
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
|
| Thu, 04 Jul 2013 23:51:47 +0200 |
wenzelm |
separate exec_id assignment for Command.print states, without affecting result of eval;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 15:19:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 16:10:46 +0100 |
wenzelm |
structural equality for Command.Results;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 16:27:44 +0100 |
wenzelm |
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 12:45:19 +0100 |
wenzelm |
discontinued obsolete 'uses' within theory header;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 13:52:18 +0100 |
wenzelm |
identify dialogs via official serial and maintain as result message;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 20:31:49 +0100 |
wenzelm |
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2012 20:35:09 +0200 |
wenzelm |
removed unused module Blob;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 15:25:49 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 19:23:04 +0200 |
wenzelm |
accumulate under exec_id as well;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 13:18:45 +0200 |
wenzelm |
some support for inital command markup;
|
file |
diff |
annotate
|
| Thu, 13 Sep 2012 16:01:42 +0200 |
wenzelm |
more efficient painting based on cached result;
|
file |
diff |
annotate
|
| Fri, 24 Aug 2012 20:41:47 +0200 |
wenzelm |
prefer jEdit file name representation (potentially via VFS);
|
file |
diff |
annotate
|
| Tue, 14 Aug 2012 12:21:32 +0200 |
wenzelm |
even more defensive path expansion (see also 8d381fdef898);
|
file |
diff |
annotate
|