src/Pure/ML/ml_file.ML
4 months ago ago clarified signature;
5 months ago ago expose generic setup of ML_File
10 months ago ago clarified environment: allow "read>write" specification;
10 months ago ago support named ML environments, notably "Isabelle", "SML";
18 months ago ago theory Pure is default presentation context;
18 months ago ago check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
2016-04-07 ago more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
2016-04-05 ago support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
2016-04-05 ago support for ML project ROOT file, with imitation of ML "use" commands;
2016-04-04 ago more uniform ML file commands;
2015-08-17 ago support for ML files with/without debugger information;
2015-08-17 ago explicit debug flag for ML compiler;
2015-08-06 ago evaluate ML expressions within debugger context;
2014-11-30 ago more abstract type Input.source;
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;