| Fri, 09 Oct 2015 19:25:13 +0200 |
wenzelm |
output HTML text according to Isabelle/Scala Symbol.Interpretation;
|
file |
diff |
annotate
|
| Thu, 20 Aug 2015 21:08:47 +0200 |
wenzelm |
clarified modules, like ML version;
|
file |
diff |
annotate
|
| Mon, 10 Aug 2015 20:42:59 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 10 Aug 2015 19:17:49 +0200 |
wenzelm |
more thorough Encode.string;
|
file |
diff |
annotate
|
| Tue, 17 Mar 2015 15:21:41 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 11:30:54 +0100 |
wenzelm |
tuned protocol -- resolve command positions in ML;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 11:07:56 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2015 21:57:10 +0100 |
wenzelm |
proper command id for inlined errors, which is important for Command.State.accumulate;
|
file |
diff |
annotate
|
| Sat, 14 Mar 2015 19:51:36 +0100 |
wenzelm |
clarified positions of theory imports;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2015 22:00:51 +0100 |
wenzelm |
clarified markup for embedded files, early before execution;
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 20:12:30 +0100 |
wenzelm |
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
|
file |
diff |
annotate
|
| Wed, 14 Jan 2015 14:28:52 +0100 |
wenzelm |
clarified build_theories;
|
file |
diff |
annotate
|
| Tue, 13 Jan 2015 21:46:09 +0100 |
wenzelm |
some support for PIDE batch session;
|
file |
diff |
annotate
|
| Tue, 30 Dec 2014 23:45:03 +0100 |
wenzelm |
explicit message channel for "legacy", which is nonetheless a variant of "warning";
|
file |
diff |
annotate
|
| Tue, 23 Dec 2014 20:46:42 +0100 |
wenzelm |
explicit message channels for "state", "information";
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 20:45:20 +0100 |
wenzelm |
clarified define_command: send tokens more directly, without requiring keywords in ML;
|
file |
diff |
annotate
|
| Wed, 20 Aug 2014 15:12:32 +0200 |
wenzelm |
default command position is only valid for default text chunk (amending dcb758188aa6);
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 18:36:43 +0200 |
wenzelm |
generic process wrapping in Prover;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 15:31:24 +0200 |
wenzelm |
clarified Position.Identified: do not require range from prover, default to command position;
|
file |
diff |
annotate
|
| Sat, 02 Aug 2014 19:29:02 +0200 |
wenzelm |
proper priority for error over warning also for node_status (see 9c5220e05e04);
|
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, 17 Apr 2014 13:21:36 +0200 |
wenzelm |
added protocol command "use_theories", with core functionality of batch build;
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 15:03:07 +0200 |
wenzelm |
more explicit message discrimination;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 21:48:09 +0200 |
wenzelm |
more direct interpretation of "warned" status, like "failed" and independently of "finished", e.g. relevant for Rendering.overview_color of aux. files where main command status is unavailable (amending 0546e036d1c0);
|
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 16:07:02 +0200 |
wenzelm |
avoid data redundancy;
|
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
|
| Mon, 07 Apr 2014 23:02:29 +0200 |
wenzelm |
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
|
file |
diff |
annotate
|
| Mon, 07 Apr 2014 13:55:12 +0200 |
wenzelm |
support for URL as file name, similar to treatment in jEdit.java;
|
file |
diff |
annotate
|
| Mon, 07 Apr 2014 13:06:34 +0200 |
wenzelm |
separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 21:55:48 +0200 |
wenzelm |
more direct warning within persistent Protocol.Status;
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 14:54:17 +0200 |
wenzelm |
more general prover operations;
|
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
|
| Wed, 02 Apr 2014 12:26:11 +0200 |
wenzelm |
persistent protocol_status, to improve performance of node_status a little;
|
file |
diff |
annotate
|
| Tue, 01 Apr 2014 23:04:22 +0200 |
wenzelm |
tuned for-comprehensions -- less structure mapping;
|
file |
diff |
annotate
|
| Tue, 01 Apr 2014 22:25:01 +0200 |
wenzelm |
some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);
|
file |
diff |
annotate
|
| 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
|