clarified future scheduling parameters, with support for parallel_limit;

allow formal comments in ML;
ML_Compiler.eval: always suppress comments;

suppress dummy id;

omit unused markup;

clarified modules;

--HG--
rename : src/HOL/Tools/value.ML => src/HOL/Tools/value_command.ML

support for Poly/ML entity ids;

proper support for recursive ML debugging;

tuned signature;
proper signature for structure;

explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
handle bootstrap signatures as well;

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;

clarified modules;
tuned signature;

clarified modules -- simplified bootstrap;

support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;

tuned signature;

tuned signature;

discontinued slightly odd "secure" mode;

clarified modules;
tuned signature;

tuned signature -- clarified modules;

clarified modules;
tuned signature;

clarified modules;

discontinued polyml-5.3.0;

--HG--
rename : src/Pure/RAW/ml_debugger_polyml-5.6.ML => src/Pure/RAW/ml_debugger.ML
rename : src/Pure/RAW/ml_name_space_polyml-5.6.ML => src/Pure/RAW/ml_name_space.ML
rename : src/Pure/RAW/ml_profiling_polyml-5.6.ML => src/Pure/RAW/ml_profiling.ML

tuned signature;

load secure.ML earlier;
eliminated obsolete ml_parse.ML;
tuned signature;

--HG--
rename : src/Pure/General/secure.ML => src/Pure/RAW/secure.ML

ML debugger support in Pure (again, see 3565c9f407ec);

support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);

clarified file names;

--HG--
rename : src/Pure/ML/exn_output_polyml.ML => src/Pure/ML/exn_output.ML
rename : src/Pure/ML/exn_properties_polyml.ML => src/Pure/ML/exn_properties.ML
rename : src/Pure/ML/ml_compiler_polyml.ML => src/Pure/ML/ml_compiler.ML

SML/NJ is no longer supported;

explicit debug flag for ML compiler;

evaluate ML expressions within debugger context;
redirected writeln/warning for ML compiler;

added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;

redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
more explicit ML_Compiler.flags;

clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;

proper configuration option "ML_print_depth";
proper ML_exception_trace for HOL-TPTP;

added command 'SML_file' for Standard ML without Isabelle/ML add-ons;

tuned signature;

improved printing of exception trace in Poly/ML 5.5.1;

prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);

tuned signature;

identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;

more careful treatment of exception serial numbers, with propagation to message channel;

more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;

added exn_message (formerly in toplevel.ML);
eval/code: proper Isar runtime support;
tuned signature;

added exception_position (dummy);

added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);