src/Pure/pure_syn.ML
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;