src/Pure/ROOT.ML
2016-04-07 wenzelm 2016-04-07 back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
2016-04-07 wenzelm 2016-04-07 clarified mode of ROOT.ML files;
2016-04-07 wenzelm 2016-04-07 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;
2016-04-07 wenzelm 2016-04-07 clarified editor mode;
2016-04-06 wenzelm 2016-04-06 virtual thread data via context, for proper support of Context.>> etc;
2016-04-06 wenzelm 2016-04-06 clarified bootstrap;
2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-04-06 wenzelm 2016-04-06 clarified ML bootstrap;
2016-04-05 wenzelm 2016-04-05 clarified files;
2016-04-05 wenzelm 2016-04-05 back to static conditional compilation -- simplified bootstrap;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2016-04-05 wenzelm 2016-04-05 actually observe ML_system_unsafe, concerning the environment that is stored in theory ML_Root;
2016-04-05 wenzelm 2016-04-05 prefer antiquotations;
2016-04-05 wenzelm 2016-04-05 proper use_thy;
2016-04-04 wenzelm 2016-04-04 more uniform ML file commands;
2016-04-04 wenzelm 2016-04-04 clarified bootstrap -- avoid conditional compilation in ROOT.ML;
2016-04-04 wenzelm 2016-04-04 tuned;
2016-04-04 wenzelm 2016-04-04 clarified modules;
2016-04-04 wenzelm 2016-04-04 clarified conditional compilation;
2016-04-04 wenzelm 2016-04-04 clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
2016-04-04 wenzelm 2016-04-04 clarified bootstrap -- more uniform use of ML files;
2016-04-04 wenzelm 2016-04-04 clarified bootstrap;
2016-04-04 wenzelm 2016-04-04 clarified final setup of ML environment;
2016-04-04 wenzelm 2016-04-04 clarified modules;
2016-04-02 wenzelm 2016-04-02 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
2016-04-02 wenzelm 2016-04-02 clarified modules;
2016-04-02 wenzelm 2016-04-02 clarified modules;
2016-03-26 wenzelm 2016-03-26 explicit print_depth for the sake of Spec_Check.determine_type;
2016-03-26 wenzelm 2016-03-26 eliminated duplicate;
2016-03-18 wenzelm 2016-03-18 discontinued slightly odd "secure" mode;
2016-03-18 wenzelm 2016-03-18 clarified modules;
2016-03-18 wenzelm 2016-03-18 clarified modules;
2016-03-17 wenzelm 2016-03-17 @{make_string} is available during Pure bootstrap;
2016-03-17 wenzelm 2016-03-17 clarified modules;
2016-03-17 wenzelm 2016-03-17 hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
2016-03-17 wenzelm 2016-03-17 obsolete;
2016-03-17 wenzelm 2016-03-17 tuned signature;
2016-03-16 wenzelm 2016-03-16 eliminated without magic name;
2016-03-10 wenzelm 2016-03-10 clarified files;
2016-03-10 wenzelm 2016-03-10 clarified files;
2016-03-09 wenzelm 2016-03-09 isabelle.Build uses ML_Process directly; isabelle_process is for batch mode only; removed unused feeder (already part of "isabelle console");
2016-03-07 wenzelm 2016-03-07 discontinued cd, pwd;
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2016-03-03 wenzelm 2016-03-03 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
2016-03-03 wenzelm 2016-03-03 discontinued polyml-5.3.0;
2016-03-02 wenzelm 2016-03-02 support for ML_exception_debugger;
2016-03-01 wenzelm 2016-03-01 clarified modules;
2016-03-01 wenzelm 2016-03-01 load secure.ML earlier; eliminated obsolete ml_parse.ML; tuned signature;
2016-03-01 wenzelm 2016-03-01 ML debugger support in Pure (again, see 3565c9f407ec);
2016-02-28 wenzelm 2016-02-28 support only polyml-5.3.0 and polyml-5.6;
2016-02-18 wenzelm 2016-02-18 unconditional Multithreading; clarified files;
2016-02-17 wenzelm 2016-02-17 tuned;
2016-02-17 wenzelm 2016-02-17 clarified file names;
2016-02-17 wenzelm 2016-02-17 SML/NJ is no longer supported;
2015-12-06 wenzelm 2015-12-06 discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6;
2015-11-20 wenzelm 2015-11-20 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
2015-11-14 haftmann 2015-11-14 separate ML module for interpretation
2015-11-10 wenzelm 2015-11-10 clarified modules;
2015-11-03 wenzelm 2015-11-03 clarified modules;