src/Pure/Isar/keyword.scala
Tue, 04 Apr 2017 23:12:08 +0200 wenzelm print like syntax of Thy_Header.header;
Tue, 04 Apr 2017 22:56:28 +0200 wenzelm more explicit types;
Tue, 06 Sep 2016 15:02:22 +0200 wenzelm tuned;
Thu, 04 Aug 2016 10:55:51 +0200 wenzelm clarified modules;
Tue, 02 Aug 2016 17:35:18 +0200 wenzelm support 'abbrevs' within theory header;
Wed, 13 Jul 2016 19:36:47 +0200 wenzelm tuned;
Mon, 11 Jul 2016 16:36:29 +0200 wenzelm explicit kind "before_command";
Sun, 10 Jul 2016 11:48:30 +0200 wenzelm support for quasi_command keywords;
Sun, 10 Jul 2016 11:18:35 +0200 wenzelm tuned signature: more uniform Keyword.spec;
Fri, 08 Jul 2016 22:22:51 +0200 wenzelm indentation in reminiscence to Proof General (see proof-indent.el);
Thu, 07 Jul 2016 21:34:56 +0200 wenzelm clarified signature;
Wed, 08 Jul 2015 15:37:32 +0200 wenzelm clarified text folds: proof ... qed counts as extra block;
Wed, 08 Jul 2015 12:09:44 +0200 wenzelm tuned;
Wed, 01 Jul 2015 21:48:46 +0200 wenzelm clarified keyword categories;
Sun, 15 Mar 2015 14:46:01 +0100 wenzelm more command categories, as in ML;
Sun, 15 Mar 2015 12:49:20 +0100 wenzelm more command categories, as in ML;
Tue, 09 Dec 2014 21:14:11 +0100 wenzelm tuned signature;
Mon, 01 Dec 2014 15:21:49 +0100 wenzelm more merge operations;
Thu, 13 Nov 2014 23:45:15 +0100 wenzelm uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Wed, 05 Nov 2014 21:59:21 +0100 wenzelm more uniform header_keywords in ML/Scala;
Wed, 05 Nov 2014 21:21:15 +0100 wenzelm tuned;
Wed, 05 Nov 2014 20:05:32 +0100 wenzelm tuned;
Wed, 05 Nov 2014 17:37:25 +0100 wenzelm clarified representation of type Keywords;
Wed, 05 Nov 2014 16:57:12 +0100 wenzelm explicit type Keyword.Keywords;
Sun, 02 Nov 2014 15:27:37 +0100 wenzelm uniform heading commands work in any context, even in theory header;
Fri, 31 Oct 2014 21:48:40 +0100 wenzelm discontinued obsolete control command category;
Tue, 28 Oct 2014 11:42:51 +0100 wenzelm explicit keyword category for commands that may start a block;
Fri, 01 Aug 2014 20:43:23 +0200 wenzelm removed unused stuff;
Fri, 01 Aug 2014 20:20:17 +0200 wenzelm agree on keyword categories with ML;
Fri, 01 Aug 2014 20:15:00 +0200 wenzelm more keyword categories (as in ML);
Fri, 14 Mar 2014 15:41:29 +0100 wenzelm discontinued somewhat pointless "thy_script" keyword kind;
Wed, 11 Sep 2013 20:16:28 +0200 wenzelm more explicit indication of 'done' as proof script element;
Mon, 02 Sep 2013 16:10:26 +0200 wenzelm more explicit indication of 'guess' as improper Isar (aka "script") element;
Mon, 25 Feb 2013 13:29:19 +0100 wenzelm discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
Mon, 20 Aug 2012 17:05:53 +0200 wenzelm some support for inlining file content into outer syntax token language;
Fri, 16 Mar 2012 21:20:23 +0100 wenzelm more abstract heading level;
Fri, 16 Mar 2012 20:33:33 +0100 wenzelm uniform keyword names within ML/Scala -- produce elisp names via external conversion;
Thu, 05 Jan 2012 14:48:41 +0100 wenzelm prefer raw_message for protocol implementation;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Wed, 10 Nov 2010 15:47:56 +0100 wenzelm eliminated obsolete heading category -- superseded by heading_level;
Wed, 10 Nov 2010 15:41:29 +0100 wenzelm added missing Keyword.THY_SCHEMATIC_GOAL;
Sun, 08 Aug 2010 19:36:31 +0200 wenzelm explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
Sat, 07 Aug 2010 22:09:52 +0200 wenzelm simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
Sat, 15 May 2010 22:05:49 +0200 wenzelm renamed Outer_Keyword to Keyword (in Scala);
less more (0) tip