Thu, 05 Nov 2015 00:02:30 +0100 |
wenzelm |
symbolic syntax "\<comment> text";
|
file |
diff |
annotate
|
Sat, 19 Sep 2015 21:07:37 +0200 |
wenzelm |
straight-forward refresh, without special preconditions;
|
file |
diff |
annotate
|
Wed, 12 Aug 2015 13:53:51 +0200 |
wenzelm |
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
|
file |
diff |
annotate
|
Sun, 03 May 2015 00:01:10 +0200 |
wenzelm |
misc tuning, based on warnings by IntelliJ IDEA;
|
file |
diff |
annotate
|
Sat, 04 Apr 2015 21:21:40 +0200 |
wenzelm |
more general notion of command span: command keyword not necessarily at start;
|
file |
diff |
annotate
|
Tue, 17 Mar 2015 15:21:41 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
Mon, 16 Mar 2015 13:32:31 +0100 |
wenzelm |
avoid duplicate header errors, more precise positions;
|
file |
diff |
annotate
|
Mon, 16 Mar 2015 11:07:56 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Sun, 15 Mar 2015 22:15:08 +0100 |
wenzelm |
more markup, which helps to create missing imports;
|
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
|
Sun, 15 Mar 2015 20:35:47 +0100 |
wenzelm |
clarified span position;
|
file |
diff |
annotate
|
Sun, 15 Mar 2015 19:21:15 +0100 |
wenzelm |
hybrid use of command blobs: inlined errors and auxiliary files;
|
file |
diff |
annotate
|
Sun, 15 Mar 2015 12:42:30 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 14 Mar 2015 21:16:29 +0100 |
wenzelm |
value-oriented user error, for well-defined Thy_Syntax.chop_common;
|
file |
diff |
annotate
|
Fri, 13 Mar 2015 12:58:49 +0100 |
wenzelm |
simplified Command.resolve_files in ML, using blobs_index from Scala;
|
file |
diff |
annotate
|
Thu, 12 Mar 2015 20:34:08 +0100 |
wenzelm |
clarified command content;
|
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
|
Mon, 01 Dec 2014 14:24:05 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 12 Aug 2014 15:46:20 +0200 |
wenzelm |
tuned;
|
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
|
Tue, 12 Aug 2014 14:15:58 +0200 |
wenzelm |
maintain Command_Range position as in ML;
|
file |
diff |
annotate
|
Tue, 12 Aug 2014 00:08:32 +0200 |
wenzelm |
separate module Command_Span: mostly syntactic representation;
|
file |
diff |
annotate
|
Mon, 11 Aug 2014 22:59:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 11 Aug 2014 22:43:26 +0200 |
wenzelm |
tuned output, in accordance to transaction name in ML;
|
file |
diff |
annotate
|
Mon, 11 Aug 2014 22:29:48 +0200 |
wenzelm |
more explicit type Span in Scala, according to ML version;
|
file |
diff |
annotate
|
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 13:01:30 +0200 |
wenzelm |
more explicit discrimination of empty nodes -- suppress from Theories panel;
|
file |
diff |
annotate
|
Tue, 29 Apr 2014 13:32:13 +0200 |
wenzelm |
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
|
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, 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:24:00 +0200 |
wenzelm |
expose more bad cases;
|
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 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:31:17 +0200 |
wenzelm |
more uniform Command.Chunk operations;
|
file |
diff |
annotate
|
Tue, 08 Apr 2014 12:19:33 +0200 |
wenzelm |
more explicit Command.Chunk types, less ooddities;
|
file |
diff |
annotate
|
Thu, 03 Apr 2014 21:55:48 +0200 |
wenzelm |
more direct warning within persistent Protocol.Status;
|
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
|
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 12:11:32 +0100 |
wenzelm |
more frugal merge of markup trees: filter wrt. subsequent query;
|
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
|
Thu, 27 Feb 2014 14:51:14 +0100 |
wenzelm |
reparse only for actually changed blobs;
|
file |
diff |
annotate
|
Wed, 26 Feb 2014 20:56:55 +0100 |
wenzelm |
tuned output;
|
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
|
Fri, 21 Feb 2014 13:36:40 +0100 |
wenzelm |
tuned signature -- avoid obscure default arguments;
|
file |
diff |
annotate
|
Thu, 20 Feb 2014 16:56:51 +0100 |
wenzelm |
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
|
file |
diff |
annotate
|
Thu, 20 Feb 2014 14:36:17 +0100 |
wenzelm |
tuned imports;
|
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 11:05:48 +0100 |
wenzelm |
more accurate eq_content;
|
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
|