| Tue, 01 Apr 2014 17:29:47 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Tue, 01 Apr 2014 17:26:32 +0200 |
wenzelm |
more frugal command_status, which is often used in a tight loop;
|
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
|
| Thu, 27 Mar 2014 19:47:30 +0100 |
wenzelm |
back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);
|
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 19:42:16 +0100 |
wenzelm |
clarified valid_id: always standardize towards static command.id;
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:54:12 +0100 |
wenzelm |
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 15:58:47 +0100 |
wenzelm |
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 12:07:26 +0100 |
wenzelm |
tuned signature -- more explicit Document.Elements;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 14:07:04 +0100 |
wenzelm |
more formal Document.Blobs;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 12:32:06 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 14:05:08 +0100 |
wenzelm |
more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 10:50:49 +0100 |
wenzelm |
clarified message_positions: cover alt_id as well;
|
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
|
| Tue, 11 Feb 2014 15:05:13 +0100 |
wenzelm |
report (but ignore) markup within auxiliary files;
|
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
|
| Wed, 20 Nov 2013 11:55:52 +0100 |
wenzelm |
load files that are not provided by PIDE blobs;
|
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 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 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
|
| Fri, 09 Aug 2013 11:18:36 +0200 |
wenzelm |
cancel_query via direct access to the exec_id of the running query process;
|
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
|
| 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
|
| Mon, 29 Jul 2013 13:00:36 +0200 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 18:13:09 +0200 |
wenzelm |
more rendering for information messages;
|
file |
diff |
annotate
|
| Wed, 10 Jul 2013 22:04:57 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 13:17:22 +0200 |
wenzelm |
tuned protocol terminology;
|
file |
diff |
annotate
|