2016-07-10 wenzelm 2016-07-10 tuned signature: more uniform Keyword.spec;
2016-07-08 wenzelm 2016-07-08 indentation in reminiscence to Proof General (see proof-indent.el);
2016-07-07 wenzelm 2016-07-07 clarified signature;
2015-07-08 wenzelm 2015-07-08 clarified text folds: proof ... qed counts as extra block;
2015-07-08 wenzelm 2015-07-08 tuned;
2015-07-01 wenzelm 2015-07-01 clarified keyword categories;
2015-03-15 wenzelm 2015-03-15 more command categories, as in ML; tuned;
2015-03-15 wenzelm 2015-03-15 more command categories, as in ML;
2014-12-09 wenzelm 2014-12-09 tuned signature;
2014-12-01 wenzelm 2014-12-01 more merge operations;
2014-11-13 wenzelm 2014-11-13 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style; discontinued obsolete 'txt_raw' (superseded by 'text_raw'); eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds); 'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind; changed tagging of diagnostic commands within proof;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-05 wenzelm 2014-11-05 more uniform header_keywords in ML/Scala; tuned signature;
2014-11-05 wenzelm 2014-11-05 tuned;
2014-11-05 wenzelm 2014-11-05 tuned;
2014-11-05 wenzelm 2014-11-05 clarified representation of type Keywords; tuned signature;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.Keywords;
2014-11-02 wenzelm 2014-11-02 uniform heading commands work in any context, even in theory header; discontinued obsolete 'sect', 'subsect', 'subsubsect'; marked obsolete 'header' as legacy;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete control command category;
2014-10-28 wenzelm 2014-10-28 explicit keyword category for commands that may start a block;
2014-08-01 wenzelm 2014-08-01 removed unused stuff;
2014-08-01 wenzelm 2014-08-01 agree on keyword categories with ML;
2014-08-01 wenzelm 2014-08-01 more keyword categories (as in ML);
2014-03-14 wenzelm 2014-03-14 discontinued somewhat pointless "thy_script" keyword kind;
2013-09-11 wenzelm 2013-09-11 more explicit indication of 'done' as proof script element;
2013-09-02 wenzelm 2013-09-02 more explicit indication of 'guess' as improper Isar (aka "script") element;
2013-02-25 wenzelm 2013-02-25 discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
2012-08-20 wenzelm 2012-08-20 some support for inlining file content into outer syntax token language;
2012-03-16 wenzelm 2012-03-16 more abstract heading level;
2012-03-16 wenzelm 2012-03-16 uniform keyword names within ML/Scala -- produce elisp names via external conversion; discontinued obsolete Keyword.thy_switch;
2012-01-05 wenzelm 2012-01-05 prefer raw_message for protocol implementation;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2010-11-10 wenzelm 2010-11-10 eliminated obsolete heading category -- superseded by heading_level;
2010-11-10 wenzelm 2010-11-10 added missing Keyword.THY_SCHEMATIC_GOAL; more keyword categories;
2010-08-08 wenzelm 2010-08-08 explicitly distinguish Output.status (essential feedback) vs. (useful markup);
2010-08-07 wenzelm 2010-08-07 simplified type XML.Tree: embed Markup directly, avoid slightly odd triple; XML.cache_tree: actually store XML.Text as well; added;
2010-05-15 wenzelm 2010-05-15 renamed Outer_Keyword to Keyword (in Scala);