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;
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;