| Wed, 23 Jul 2014 18:14:59 +0200 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Wed, 28 May 2014 16:16:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 20 May 2014 20:05:43 +0200 |
wenzelm |
afford strict check (see also AFP/a8e08d947f0a);
|
file |
diff |
annotate
|
| Mon, 12 May 2014 12:31:33 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Wed, 07 May 2014 12:59:15 +0200 |
wenzelm |
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2014 14:41:52 +0100 |
wenzelm |
prefer Context_Position where a context is available;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 13:36:28 +0100 |
wenzelm |
clarified bootstrap process: switch to ML with context and antiquotations earlier;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 10:17:29 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 14:44:43 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 12:09:51 +0100 |
wenzelm |
explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;
|
file |
diff |
annotate
|
| Fri, 13 Dec 2013 12:31:45 +0100 |
wenzelm |
clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 16:58:35 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 16:19:57 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 05 Apr 2013 20:54:55 +0200 |
wenzelm |
tuned signature -- agree with markup terminology;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2013 12:17:11 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Sun, 24 Feb 2013 17:29:55 +0100 |
wenzelm |
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 00:00:42 +0100 |
wenzelm |
support nested Thy_Syntax.element;
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 13:52:33 +0100 |
wenzelm |
generalized notion of active area, where sendback is just one application;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 16:16:47 +0100 |
wenzelm |
more general sendback properties;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 13:54:43 +0100 |
wenzelm |
refined outer syntax 'help' command;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2012 18:24:49 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Fri, 24 Aug 2012 12:35:39 +0200 |
wenzelm |
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
|
file |
diff |
annotate
|
| Mon, 20 Aug 2012 14:09:09 +0200 |
wenzelm |
added keyword kind "thy_load" (with optional list of file extensions);
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 18:05:41 +0200 |
wenzelm |
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 17:24:21 +0200 |
wenzelm |
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
|
file |
diff |
annotate
|
| Thu, 09 Aug 2012 22:31:04 +0200 |
wenzelm |
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 13:37:58 +0200 |
wenzelm |
report commands as formal entities, with def/ref positions;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 12:36:54 +0200 |
wenzelm |
more official command specifications, including source position;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2012 19:53:20 +0200 |
wenzelm |
more standard bootstrapping of Pure.thy;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2012 15:40:57 +0200 |
wenzelm |
internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;
|
file |
diff |
annotate
|
| Tue, 10 Apr 2012 21:31:05 +0200 |
wenzelm |
static relevance of proof via syntax keywords;
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 18:18:42 +0100 |
wenzelm |
allow keyword tags to be redefined, but not the command category;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 21:40:21 +0100 |
wenzelm |
check declared vs. defined commands at end of session;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 13:05:30 +0100 |
wenzelm |
define keywords early when processing the theory header, before running the body commands;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 11:26:55 +0100 |
wenzelm |
clarified Keyword.is_keyword: union of minor and major;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 17:27:52 +0100 |
wenzelm |
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 20:37:07 +0200 |
wenzelm |
bulk reports for improved message throughput;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 20:35:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 20:29:39 +0200 |
wenzelm |
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 19:12:58 +0200 |
wenzelm |
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 20:42:26 +0200 |
wenzelm |
tuned Parse.group: delayed failure message;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 20:49:41 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special name argument;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 20:41:29 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special master argument;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 21:44:47 +0200 |
wenzelm |
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 20:27:09 +0200 |
wenzelm |
less stateful outer_syntax;
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 17:36:25 +0200 |
wenzelm |
clarified Thy_Syntax.element;
|
file |
diff |
annotate
|
| Sat, 26 Mar 2011 21:45:29 +0100 |
wenzelm |
present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 21:28:11 +0100 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
file |
diff |
annotate
|
| Sat, 05 Feb 2011 20:38:32 +0100 |
wenzelm |
more tracing information via Par_List.map_name;
|
file |
diff |
annotate
|
| Thu, 13 Jan 2011 17:34:45 +0100 |
wenzelm |
Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
|
file |
diff |
annotate
|
| Sun, 09 Jan 2011 20:30:47 +0100 |
wenzelm |
more direct treatment of Position.end_offset;
|
file |
diff |
annotate
|
| Sat, 13 Nov 2010 19:21:53 +0100 |
wenzelm |
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
|
file |
diff |
annotate
|
| Sun, 15 Aug 2010 20:19:56 +0200 |
wenzelm |
rename "unit" to "atom", to avoid confusion with the unit type;
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 18:18:32 +0200 |
wenzelm |
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
|
file |
diff |
annotate
|
| Sun, 08 Aug 2010 19:36:31 +0200 |
wenzelm |
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
|
file |
diff |
annotate
|