src/Pure/Isar/keyword.ML
3 months ago wenzelm 2019-03-14 more specific keyword kinds;
18 months ago wenzelm 2017-12-05 explicit tag for document commands: avoid implicit use of document_tags;
2016-07-11 wenzelm 2016-07-11 explicit kind "before_command"; tuned signature;
2016-07-10 wenzelm 2016-07-10 support for quasi_command keywords;
2016-07-10 wenzelm 2016-07-10 tuned signature: more uniform Keyword.spec;
2015-11-10 wenzelm 2015-11-10 more thorough check_command, including completion;
2015-07-08 wenzelm 2015-07-08 clarified text folds: proof ... qed counts as extra block;
2015-07-08 wenzelm 2015-07-08 more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
2015-07-01 wenzelm 2015-07-01 clarified keyword categories;
2015-04-06 wenzelm 2015-04-06 clarified command keyword markup;
2015-04-06 wenzelm 2015-04-06 more position information and PIDE markup for command keywords;
2015-03-17 wenzelm 2015-03-17 misc tuning and simplification;
2015-03-15 wenzelm 2015-03-15 more command categories, as in ML; tuned;
2014-12-10 wenzelm 2014-12-10 more explicit markup for improper commands; clarified CSS rendering;
2014-12-09 wenzelm 2014-12-09 imitate command markup and rendering of Isabelle/jEdit in HTML output;
2014-11-22 wenzelm 2014-11-22 tuned signature;
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 clarified keyword categories; tuned;
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-06 wenzelm 2014-11-06 tuned signature;
2014-11-06 wenzelm 2014-11-06 more explicit Keyword.keywords;
2014-11-06 wenzelm 2014-11-06 tuned signature;
2014-11-06 wenzelm 2014-11-06 prefer explicit Keyword.keywords;
2014-11-06 wenzelm 2014-11-06 simplified keyword kinds; more explicit bootstrap syntax;
2014-11-05 wenzelm 2014-11-05 tuned;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.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-05-13 wenzelm 2014-05-13 no reset for 'end' -- e.g. relevant for 'notepad';
2014-05-07 wenzelm 2014-05-07 discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
2014-03-14 wenzelm 2014-03-14 discontinued somewhat pointless "thy_script" keyword kind;
2013-11-19 wenzelm 2013-11-19 more uniform handling of inlined files;
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-06-24 wenzelm 2013-06-24 obsolete -- cf. isabelle.Keywords in Scala;
2013-02-25 wenzelm 2013-02-25 discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
2013-02-20 wenzelm 2013-02-20 support nested Thy_Syntax.element; more explicit Keyword.is_proof_body; tuned;
2013-01-04 wenzelm 2013-01-04 more formal inlining of system information;
2012-08-23 wenzelm 2012-08-23 tuned signature (again, cf. ff9cd47be39b);
2012-08-23 wenzelm 2012-08-23 simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
2012-08-21 wenzelm 2012-08-21 refined Thy_Load.check_thy: find more uses in body text, based on keywords; refined Thy_Info.require_thy(s): cumulate additional keywords; slightly more value-oriented type Keywords.keywords;
2012-08-21 wenzelm 2012-08-21 some support for thy_load_commands; clarified signatures;
2012-08-20 wenzelm 2012-08-20 some support for inlining file content into outer syntax token language;
2012-08-20 wenzelm 2012-08-20 added keyword kind "thy_load" (with optional list of file extensions);
2012-08-07 wenzelm 2012-08-07 prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol; just one cumulative Keyword.status at end of batch session;
2012-08-02 wenzelm 2012-08-02 more official command specifications, including source position;
2012-03-16 wenzelm 2012-03-16 more abstract heading level;
2012-03-16 wenzelm 2012-03-16 less redundant data;
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-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-16 wenzelm 2012-03-16 define keywords early when processing the theory header, before running the body commands;
2012-03-16 wenzelm 2012-03-16 clarified Keyword.is_keyword: union of minor and major; misc tuning and simplification;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 wenzelm 2012-03-15 declare keywords as side-effect of header edit; parse_command span is now lazy instead of future, to happen synchronously after header edit in new_exec (before execution);
2012-03-15 wenzelm 2012-03-15 some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.;
2012-03-14 wenzelm 2012-03-14 tuned;
2012-03-03 wenzelm 2012-03-03 clarified terminology of raw protocol messages;
2012-01-05 wenzelm 2012-01-05 prefer raw_message for protocol implementation;