2013-10-16 ago avoid non-portable int constant -- make SML/NJ happy;
2013-09-18 ago improved printing of exception trace in Poly/ML 5.5.1;
2013-01-16 ago more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2013-01-16 ago tuned comments;
2012-07-21 ago more ML_System operations;
2011-08-17 ago identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
2011-07-23 ago explicit structure ML_System;
2011-06-30 ago getenv_strict in ML;
2011-04-08 ago discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
2011-03-20 ago structure Timing: covers former start_timing/end_timing and Output.timeit etc;
2010-12-29 ago share_common_data dummy;
2010-11-27 ago removed bash from ML system bootstrap, and past the Secure ML barrier;
2010-11-20 ago renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-06 ago somewhat more uniform timing in ML vs. Scala;
2010-09-22 ago renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
2010-09-22 ago main Isabelle_Process via Isabelle_System.Managed_Process;
2010-09-09 ago Exn.is_interrupt: include interrupts that have passed through the IO layer;
2010-09-09 ago more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-08-23 ago added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
2010-04-16 ago added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
2010-02-06 ago explicit representation of single-assignment variables;
2010-02-06 ago renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
2009-12-19 ago added basic library -- Scala version;
2009-10-22 ago support single-assigment variables -- based on magic RTS operations by David Matthews;
2009-09-30 ago more uniform treatment of structure Unsynchronized in ML bootstrap phase;
2009-09-29 ago Raw ML references as unsynchronized state variables.
2009-06-17 ago more detailed start_timing/end_timing (in timing.ML);
2009-06-04 ago reraise exceptions to preserve original position (ML system specific);
2009-05-31 ago eliminated misleading dummy versions of print/makestring, cf. 6974449ddea9;
2009-03-23 ago more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
2009-03-21 ago adapted toplevel_pp to ML_Pretty.pretty;
2009-03-21 ago added generic ML_Pretty interface;
2009-03-01 ago end_timing: generalized result -- message plus with explicit time values;
2009-01-19 ago removed Ids;
2008-10-03 ago removed obsolete Posix/Signal compatibility wrappers;
2008-10-01 ago more robust treatment of Interrupt (cf. exn.ML);
2008-09-17 ago use_text/use_file now depend on explicit ML name space;
2008-09-17 ago use_text/use_file now depend on explicit ML name space;
2008-09-07 ago explicit use of universal.ML and dummy_thread.ML;
2008-05-14 ago use_file: pass str_of_pos;
2008-05-14 ago use_text/file: ignore str_of_pos argument;
2008-03-31 ago before close: Exn.capture/release;
2008-03-28 ago added forget_structure;
2008-03-24 ago ML runtime compilation: pass position, tuned signature;
2008-03-06 ago common setup for system_out/system;
2008-02-16 ago replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
2007-12-20 ago added ML-Systems/universal.ML;
2007-09-24 ago replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
2007-09-16 ago use_text/file: tune text (cf. ML_Parse.fix_ints);
2007-08-18 ago ML system provides get_print_depth;
2007-08-15 ago tuned comments;
2007-08-03 ago preparations for proper type int;
2007-07-24 ago ML-Systems/exn.ML, ML-Systems/multithreading_dummy.ML;
2007-07-23 ago added compatibility file for ML systems without multithreading;
2007-07-17 ago moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
2007-07-11 ago added dummy makestring function
2007-05-31 ago TextIO.inputLine: use present SML B library version;
2007-01-21 ago use_text: added name argument;
2006-12-11 ago added use_file;
2006-11-10 ago tuned names of start_timing,/end_timing/check_timer;