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;
2014-08-12 wenzelm 2014-08-12 separate module Command_Span: mostly syntactic representation; potentially prover-specific Output_Syntax.parse_spans;
2014-07-24 wenzelm 2014-07-24 further distinction of Isabelle distribution: alert for identified release candidates;
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-04-06 wenzelm 2014-04-06 clarified ML bootstrap;
2014-03-27 wenzelm 2014-03-27 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-26 wenzelm 2014-03-26 tuned comments;
2014-03-26 wenzelm 2014-03-26 tuned load order;
2014-03-25 wenzelm 2014-03-25 proper configuration option "ML_print_depth"; proper ML_exception_trace for HOL-TPTP;
2014-03-20 wenzelm 2014-03-20 tuned error, according to "use" in General/secure.ML;
2014-03-18 wenzelm 2014-03-18 clarified module arrangement;
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-03-18 wenzelm 2014-03-18 clarified module arrangement; more antiquotations;
2014-03-18 wenzelm 2014-03-18 clarified modules; more antiquotations for antiquotations;
2014-03-18 wenzelm 2014-03-18 clarified bootstrap process: switch to ML with context and antiquotations earlier;
2014-03-12 wenzelm 2014-03-12 tuned signature -- clarified module name;
2014-03-11 wenzelm 2014-03-11 tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
2014-02-22 wenzelm 2014-02-22 support for completion within the formal context; tuned signature;
2014-02-16 wenzelm 2014-02-16 prefer user-space tool within Pure.thy;
2014-02-10 wenzelm 2014-02-10 seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
2014-01-25 wenzelm 2014-01-25 prefer self-contained user-space tool;
2014-01-17 wenzelm 2014-01-17 prefer user-space tool within Pure.thy;
2013-12-13 wenzelm 2013-12-13 maintain morphism names for diagnostic purposes;
2013-12-11 wenzelm 2013-12-11 support for polml-5.5.2; support Thread.numPhysicalProcessors of polyml-5.5.2 (according to SVN 1890); clarified max_threads: store plain value internally, reproduce result only on startup, and thus avoid potential system overhead;
2013-11-16 wenzelm 2013-11-16 toplevel function "use" refers to raw ML bootstrap environment;