src/Pure/Isar/isar_cmd.ML
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;
2013-03-30 ago item markup for Proof_Context.pretty_fact;
2013-01-05 ago tuned -- less indirection;
2012-10-17 ago more method position information, notably finished_pos after end of previous text;
2012-10-16 ago more proof method text position information;
2012-09-26 ago tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
2012-09-25 ago separate module Graph_Display;
2012-08-30 ago refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
2012-08-24 ago check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
2012-08-22 ago clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-14 ago support for 'typ' with explicit sort constraint;
2012-08-11 ago faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
2012-04-27 ago clarified signature;
2012-03-14 ago source positions for locale and class expressions;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-11-14 ago pass positions for named targets, for formal links in the document model;
2011-10-28 ago uniform Local_Theory.declaration with explicit params;
2011-08-20 ago refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-06-27 ago document antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-27 ago ML antiquotations are managed as theory data, with proper name space and entity markup;
2011-04-23 ago proper binding/report of defined simprocs;
2011-04-20 ago added Theory.nodes_of convenience;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago prefer local name spaces;
2011-04-16 ago Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-06 ago typed_print_translation: discontinued show_sorts argument;
2011-04-06 ago renamed Standard_Syntax to Syntax_Phases;
2011-04-05 ago moved decode/parse operations to standard_syntax.ML;