2014-03-25 ago added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-18 ago clarifed module name;
2014-03-18 ago more antiquotations;
2014-03-01 ago clarified language markup: added "delimited" property;
2014-02-27 ago store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
2013-11-16 ago tuned signature -- clarified Proof General legacy;
2013-07-07 ago tuned comments;
2013-06-26 ago more position information for markup;
2012-08-23 ago clarified type Token.file;
2012-08-23 ago simplified Thy_Load.provide: do not store full path;
2012-08-22 ago clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-22 ago clarified bootstrapping of Pure;