src/Pure/Isar/isar_cmd.ML
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;
2011-04-05 ago discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-04-03 ago added Position.reports convenience;
2011-01-06 ago Diagnostic command to show locale dependencies.
2010-11-28 ago added 'syntax_declaration' command;
2010-11-27 ago more explicit Isabelle_System operations;
2010-11-06 ago mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 ago tuned signature of (Context_)Position.report variants;
2010-09-06 ago discontinued obsolete ProofContext.prems_limit;
2010-09-03 ago pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
2010-08-30 ago tuned;
2010-08-11 ago prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
2010-08-03 ago eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;
2010-07-31 ago print_interps shows interpretations in proofs.
2010-07-27 ago simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
2010-07-25 ago simplified handling of theory begin/end wrt. toplevel and theory loader;
2010-07-25 ago Thy_Load.check_loaded via Theory.at_end;
2010-07-24 ago moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
2010-07-21 ago thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
2010-07-21 ago thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here -- also avoid referring to accidental theory loader state;
2010-06-03 ago diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-30 ago replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
2010-05-27 ago renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-05-08 ago unified/simplified Pretty.margin_default;
2010-04-25 ago replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-04-25 ago modernized naming conventions of main Isar proof elements;
2010-04-16 ago keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;