src/Pure/ROOT.ML
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;
2015-10-15 wenzelm 2015-10-15 load markdown.ML into Pure;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-24 wenzelm 2015-09-24 more explicit Defs.context: use proper name spaces as far as possible;
2015-08-17 wenzelm 2015-08-17 basic setup for native Windows (RAW session without image);
2015-08-17 wenzelm 2015-08-17 no ML_debugger support in Pure -- too complicated;
2015-08-17 wenzelm 2015-08-17 more careful propagation of ML_debugger option to Pure;
2015-08-17 wenzelm 2015-08-17 support for ML files with/without debugger information;
2015-08-17 wenzelm 2015-08-17 explicit debug flag for ML compiler;
2015-08-15 wenzelm 2015-08-15 clarified context;
2015-08-12 wenzelm 2015-08-12 default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
2015-07-02 wenzelm 2015-07-02 clarified module;
2015-04-01 wenzelm 2015-04-01 added command 'experiment';
2015-03-16 wenzelm 2015-03-16 tuned protocol -- resolve command positions in ML;
2015-01-29 wenzelm 2015-01-29 tuned bootstrap;
2015-01-14 wenzelm 2015-01-14 added Path.decode in ML, in correspondence to Path.encode in Scala;
2014-12-30 wenzelm 2014-12-30 explicit message channel for "legacy", which is nonetheless a variant of "warning";
2014-12-29 wenzelm 2014-12-29 more toplevel pretty printing;
2014-12-22 wenzelm 2014-12-22 separate module Random; proper Synchronized.var;
2014-12-03 wenzelm 2014-12-03 node-specific keywords, with session base syntax as default;
2014-11-30 wenzelm 2014-11-30 more abstract type Input.source;
2014-11-26 wenzelm 2014-11-26 load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
2014-11-21 wenzelm 2014-11-21 removed some add-ons from modules that are relevant for the inference kernel;
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-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-10-31 wenzelm 2014-10-31 discontinued Isar TTY loop;
2014-10-31 wenzelm 2014-10-31 discontinued Proof General;
2014-10-13 wenzelm 2014-10-13 obsolete;
2014-10-13 wenzelm 2014-10-13 clarified load order; tuned signature;
2014-09-29 wenzelm 2014-09-29 pro-forma support for polyml-5.5.3 (presently SVN 1960);
2014-08-22 wenzelm 2014-08-22 clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;
2014-08-19 wenzelm 2014-08-19 clarified modules;
2014-08-14 wenzelm 2014-08-14 tuned signature -- prefer self-contained user-space tool;
2014-08-13 wenzelm 2014-08-13 load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;