src/Pure/Isar/isar_cmd.ML
4 months ago ago clarified Toplevel.state: more explicit types;
8 months ago ago clarified ML positions (see also 1a52baa70aed);
8 months ago ago clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
8 months ago ago clarified ML position: proper markup for def/ref scopes (see also 162a4c2e97bc);
10 months ago ago clarified signature;
18 months ago ago clarified signature;
19 months ago ago prefer control symbol antiquotations;
2017-02-04 ago more uniform use of Reconstruct.clean_proof_of;
2016-08-06 ago more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
2016-04-09 ago clarified context;
2016-04-08 ago eliminated unused simproc identifier;
2016-01-13 ago removed old 'defs' command;
2015-09-25 ago proper context;
2015-09-09 ago simplified simproc programming interfaces;
2015-09-02 ago tuned message;
2015-07-08 ago more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
2015-06-09 ago eliminated dead code;
2015-06-09 ago tuned signature;
2015-06-07 ago tuned signature;
2015-04-16 ago tuned;
2015-04-16 ago discontinued pointless warnings: commands are only defined inside a theory context;
2015-04-16 ago explicit error for Toplevel.proof_of;
2015-04-16 ago clarified thy_deps;
2015-04-15 ago session graph with folded base theories, as in document preparation;
2015-04-06 ago tuned signature;
2015-04-03 ago more uniform "verbose" option to print name space;
2014-12-31 ago clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
2014-12-31 ago for graph display, prefer graph data structure over list with dependencies;
2014-12-31 ago more explict and generic field names
2014-12-31 ago uniform variable name for presentation graphs, to distinguish from values of type Graph.T
2014-11-30 ago tuned signature;
2014-11-30 ago more abstract type Input.source;
2014-11-22 ago more careful ML source positions, for improved PIDE markup;
2014-11-12 ago more careful ML source positions, for improved PIDE markup;
2014-11-11 ago more careful ML source positions, for improved PIDE markup;
2014-11-11 ago more position information, e.g. relevant for errors in generated ML source;
2014-11-07 ago plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
2014-11-02 ago clarified legacy command;
2014-11-02 ago uniform heading commands work in any context, even in theory header;
2014-09-07 ago separated class_deps command into separate file
2014-08-19 ago tuned signature -- moved type src to Token, without aliases;
2014-08-14 ago tuned signature -- prefer self-contained user-space tool;
2014-07-25 ago old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;
2014-07-22 ago tuned messages;
2014-05-05 ago clarified print operations for "terms" and "theorems";
2014-03-31 ago some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-27 ago redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
2014-03-25 ago separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-25 ago added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-18 ago more antiquotations;
2014-03-15 ago more explicit treatment of verbose mode, which includes concealed entries;
2014-03-15 ago clarified print_local_facts;
2014-03-12 ago tuned signature -- clarified module name;
2014-03-09 ago more formal read_root;
2014-03-09 ago simplified / modernized hide commands: proper outer parsers and PIDE markup via check;
2014-03-01 ago clarified language markup: added "delimited" property;
2013-08-23 ago added Theory.setup convenience;
2013-07-07 ago discontinued command 'print_drafts';
2013-05-25 ago syntax translations always depend on context;
2013-04-18 ago simplifier uses proper Proof.context instead of historic type simpset;