src/Pure/Isar/outer_syntax.ML
Thu, 06 Nov 2014 11:44:41 +0100 wenzelm simplified keyword kinds;
Wed, 05 Nov 2014 22:17:05 +0100 wenzelm tuned signature;
Wed, 05 Nov 2014 20:49:30 +0100 wenzelm eliminated pointless dynamic keywords (TTY legacy);
Wed, 05 Nov 2014 20:20:57 +0100 wenzelm explicit type Keyword.keywords;
Mon, 03 Nov 2014 14:50:27 +0100 wenzelm eliminated unused int_only flag (see also c12484a27367);
Sat, 01 Nov 2014 19:33:51 +0100 wenzelm recover via scanner;
Sat, 01 Nov 2014 18:46:48 +0100 wenzelm simplified -- scanning is never interactive;
Sat, 01 Nov 2014 15:35:40 +0100 wenzelm tuned signature, in accordance to Scala version;
Sat, 01 Nov 2014 15:01:41 +0100 wenzelm command-line terminator ";" is no longer accepted;
Fri, 31 Oct 2014 22:02:49 +0100 wenzelm discontinued obsolete \<^sync> marker;
Fri, 31 Oct 2014 21:10:11 +0100 wenzelm discontinued obsolete tty and prompt;
Tue, 12 Aug 2014 20:18:27 +0200 wenzelm tuned signature according to Scala version -- prefer explicit argument;
Tue, 12 Aug 2014 00:08:32 +0200 wenzelm separate module Command_Span: mostly syntactic representation;
Wed, 23 Jul 2014 18:14:59 +0200 wenzelm more markup;
Wed, 28 May 2014 16:16:40 +0200 wenzelm tuned signature;
Tue, 20 May 2014 20:05:43 +0200 wenzelm afford strict check (see also AFP/a8e08d947f0a);
Mon, 12 May 2014 12:31:33 +0200 wenzelm tuned message;
Wed, 07 May 2014 12:59:15 +0200 wenzelm discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
Mon, 31 Mar 2014 12:35:39 +0200 wenzelm some shortcuts for chunks, which sometimes avoid bulky string output;
Wed, 26 Mar 2014 14:41:52 +0100 wenzelm prefer Context_Position where a context is available;
Tue, 18 Mar 2014 13:36:28 +0100 wenzelm clarified bootstrap process: switch to ML with context and antiquotations earlier;
Mon, 24 Feb 2014 10:17:29 +0100 wenzelm tuned signature;
Fri, 14 Feb 2014 14:44:43 +0100 wenzelm tuned message;
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;
Fri, 13 Dec 2013 12:31:45 +0100 wenzelm clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;
Wed, 03 Jul 2013 16:58:35 +0200 wenzelm tuned signature;
Wed, 03 Jul 2013 16:19:57 +0200 wenzelm tuned signature;
Fri, 05 Apr 2013 20:54:55 +0200 wenzelm tuned signature -- agree with markup terminology;
Mon, 25 Feb 2013 12:17:11 +0100 wenzelm tuned comment;
Sun, 24 Feb 2013 17:29:55 +0100 wenzelm simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
Wed, 20 Feb 2013 00:00:42 +0100 wenzelm support nested Thy_Syntax.element;
Mon, 10 Dec 2012 13:52:33 +0100 wenzelm generalized notion of active area, where sendback is just one application;
Mon, 26 Nov 2012 16:16:47 +0100 wenzelm more general sendback properties;
Mon, 26 Nov 2012 13:54:43 +0100 wenzelm refined outer syntax 'help' command;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Tue, 25 Sep 2012 18:24:49 +0200 wenzelm tuned;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Fri, 24 Aug 2012 12:35:39 +0200 wenzelm check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
Mon, 20 Aug 2012 14:09:09 +0200 wenzelm added keyword kind "thy_load" (with optional list of file extensions);
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;
Sat, 11 Aug 2012 17:24:21 +0200 wenzelm clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
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;
Thu, 02 Aug 2012 13:37:58 +0200 wenzelm report commands as formal entities, with def/ref positions;
Thu, 02 Aug 2012 12:36:54 +0200 wenzelm more official command specifications, including source position;
Wed, 01 Aug 2012 19:53:20 +0200 wenzelm more standard bootstrapping of Pure.thy;
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;
Tue, 10 Apr 2012 21:31:05 +0200 wenzelm static relevance of proof via syntax keywords;
Mon, 19 Mar 2012 18:18:42 +0100 wenzelm allow keyword tags to be redefined, but not the command category;
Fri, 16 Mar 2012 21:40:21 +0100 wenzelm check declared vs. defined commands at end of session;
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Fri, 16 Mar 2012 13:05:30 +0100 wenzelm define keywords early when processing the theory header, before running the body commands;
Fri, 16 Mar 2012 11:26:55 +0100 wenzelm clarified Keyword.is_keyword: union of minor and major;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
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);
Tue, 06 Sep 2011 20:37:07 +0200 wenzelm bulk reports for improved message throughput;
Fri, 02 Sep 2011 20:35:32 +0200 wenzelm tuned;
Fri, 02 Sep 2011 20:29:39 +0200 wenzelm more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
Thu, 25 Aug 2011 19:12:58 +0200 wenzelm tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
Sun, 21 Aug 2011 20:42:26 +0200 wenzelm tuned Parse.group: delayed failure message;
Sat, 13 Aug 2011 20:49:41 +0200 wenzelm simplified Toplevel.init_theory: discontinued special name argument;
less more (0) -100 -60 tip