2016-12-13 wenzelm 2016-12-13 more symbols;
2016-04-07 wenzelm 2016-04-07 section headings for ROOT.ML;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2016-02-28 wenzelm 2016-02-28 discontinued old 'header';
2015-10-17 wenzelm 2015-10-17 more uniform command setup;
2015-10-17 wenzelm 2015-10-17 added 'paragraph', 'subparagraph';
2015-10-16 wenzelm 2015-10-16 clarified Antiquote.antiq_reports; Thy_Output.output_text: support for markdown (inactive); eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;
2015-08-28 wenzelm 2015-08-28 clarified language context, e.g. relevant for symbols;
2015-04-22 wenzelm 2015-04-22 tuned signature;
2015-04-16 wenzelm 2015-04-16 tuned comment;
2015-04-16 wenzelm 2015-04-16 more explicit bootstrap_thy; clarified error;
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 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 simplified keyword kinds; more explicit bootstrap syntax;
2014-10-31 wenzelm 2014-10-31 obsolete;
2014-10-31 wenzelm 2014-10-31 discontinued Proof General;
2014-05-07 wenzelm 2014-05-07 discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
2014-04-19 wenzelm 2014-04-19 added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
2014-03-27 wenzelm 2014-03-27 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); more explicit ML_Compiler.flags;
2014-03-25 wenzelm 2014-03-25 added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-03-18 wenzelm 2014-03-18 more antiquotations;
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-02-27 wenzelm 2014-02-27 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing; integrity check of SHA1 digests produced in Scala vs. ML; tuned signature;
2013-11-16 wenzelm 2013-11-16 tuned signature -- clarified Proof General legacy;
2013-07-07 wenzelm 2013-07-07 tuned comments;
2013-06-26 wenzelm 2013-06-26 more position information for markup;
2012-08-23 wenzelm 2012-08-23 clarified type Token.file;
2012-08-23 wenzelm 2012-08-23 simplified Thy_Load.provide: do not store full path;
2012-08-22 wenzelm 2012-08-22 clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-22 wenzelm 2012-08-22 clarified bootstrapping of Pure;