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 16:56:03 +0200 |
wenzelm |
more frugal edits;
|
file |
diff |
annotate
|
Wed, 23 Jul 2014 16:20:07 +0200 |
wenzelm |
more explicit treatment of cleared nodes (removal is implicit);
|
file |
diff |
annotate
|
Wed, 23 Jul 2014 15:32:05 +0200 |
wenzelm |
clarified display;
|
file |
diff |
annotate
|
Wed, 23 Jul 2014 15:00:46 +0200 |
wenzelm |
clarified display;
|
file |
diff |
annotate
|
Wed, 23 Jul 2014 14:50:20 +0200 |
wenzelm |
avoid redundant data structure;
|
file |
diff |
annotate
|
Wed, 23 Jul 2014 13:01:30 +0200 |
wenzelm |
more explicit discrimination of empty nodes -- suppress from Theories panel;
|
file |
diff |
annotate
|
Wed, 23 Jul 2014 11:53:34 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 23 Jul 2014 10:02:19 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 30 Apr 2014 22:34:11 +0200 |
wenzelm |
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
|
file |
diff |
annotate
|
Sat, 26 Apr 2014 13:34:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 26 Apr 2014 13:07:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 24 Apr 2014 23:21:00 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 15 Apr 2014 16:44:06 +0200 |
wenzelm |
clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
|
file |
diff |
annotate
|
Thu, 10 Apr 2014 14:36:29 +0200 |
wenzelm |
ignore other_id reports for now (see 8eda56033203): massive amounts of redirections to 'class' etc. makes it difficult to edit main HOL;
|
file |
diff |
annotate
|
Wed, 09 Apr 2014 10:44:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 08 Apr 2014 22:01:08 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 08 Apr 2014 20:03:00 +0200 |
wenzelm |
simplified Text.Chunk -- eliminated ooddities;
|
file |
diff |
annotate
|
Tue, 08 Apr 2014 19:17:28 +0200 |
wenzelm |
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
|
file |
diff |
annotate
|
Tue, 08 Apr 2014 15:12:54 +0200 |
wenzelm |
tuned signature -- moved Command.Chunk to Text.Chunk;
|
file |
diff |
annotate
|
Tue, 08 Apr 2014 12:19:33 +0200 |
wenzelm |
more explicit Command.Chunk types, less ooddities;
|
file |
diff |
annotate
|
Fri, 04 Apr 2014 10:41:53 +0200 |
wenzelm |
afford larger full_index, to save a few milliseconds during rendering (notably text_overview);
|
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
|
Tue, 01 Apr 2014 20:22:25 +0200 |
wenzelm |
more direct command states -- merge_results is hardly ever needed;
|
file |
diff |
annotate
|
Mon, 31 Mar 2014 15:34:37 +0200 |
wenzelm |
tuned output;
|
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 09:34:51 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 27 Mar 2014 21:18:14 +0100 |
wenzelm |
tuned -- avoid code duplication;
|
file |
diff |
annotate
|
Thu, 27 Mar 2014 12:11:32 +0100 |
wenzelm |
more frugal merge of markup trees: filter wrt. subsequent query;
|
file |
diff |
annotate
|
Thu, 27 Mar 2014 11:19:31 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 27 Mar 2014 10:43:43 +0100 |
wenzelm |
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
|
file |
diff |
annotate
|
Wed, 26 Mar 2014 21:01:09 +0100 |
wenzelm |
tuned signature -- expose less intermediate information;
|
file |
diff |
annotate
|
Wed, 26 Mar 2014 19:42:16 +0100 |
wenzelm |
clarified valid_id: always standardize towards static command.id;
|
file |
diff |
annotate
|
Mon, 17 Mar 2014 14:37:23 +0100 |
wenzelm |
tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;
|
file |
diff |
annotate
|
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
|