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