src/Pure/ML-Systems/polyml.ML
2008-05-14 wenzelm 2008-05-14 use_text/file: proper position output;
2008-05-13 wenzelm 2008-05-13 adapted PolyML.compiler to latest change of basis/FinalPolyML.sml (2008-04-21);
2008-04-10 wenzelm 2008-04-10 use_text: explicitly print exception, which is no longer done by the new PolyML.compiler setup;
2008-03-31 wenzelm 2008-03-31 before close: Exn.capture/release;
2008-03-25 wenzelm 2008-03-25 moved multithreaded "profile" to multithreading_polyml.ML;
2008-03-24 wenzelm 2008-03-24 ML runtime compilation: pass position, tuned signature;
2008-03-24 wenzelm 2008-03-24 updated use_text/file for 5.2;
2008-03-06 wenzelm 2008-03-06 rearrangements to make latest Poly/ML the default, not old 4.x;
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-10-20 wenzelm 2007-10-20 discontinued support for 4.1.1, 4.1.2; maintain PolyML.Compiler.printInAlphabeticalOrder;
2007-10-13 wenzelm 2007-10-13 PolyML.Compiler.maxInlineSize := 80;
2007-10-04 wenzelm 2007-10-04 tuned;
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 added ml_system_fix_ints; use_text/file: tune text (cf. ML_Parse.fix_ints);
2007-08-18 wenzelm 2007-08-18 ML system provides get_print_depth;
2007-08-16 wenzelm 2007-08-16 removed signal setup from root function to on-entry hook;
2007-08-15 wenzelm 2007-08-15 tuned comments;
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-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-12-08 wenzelm 2006-12-08 tuned use_text; eval command line: skip over -q option;
2006-11-10 wenzelm 2006-11-10 tuned names of start_timing,/end_timing/check_timer; removed obsolete ML compatibility fragments;
2006-11-10 wenzelm 2006-11-10 no special treatment for cygwin (this is supposed to be actual cygwin, not win32 polyml within cygwin);
2006-01-27 webertj 2006-01-27 interrupt_timeout for Poly replaced by stub
2006-01-23 webertj 2006-01-23 TimeLimit replaced by interrupt_timeout
2005-12-23 wenzelm 2005-12-23 backpatching of Substring.full;
2005-10-11 wenzelm 2005-10-11 added string_of_pid;
2005-08-16 wenzelm 2005-08-16 added String.isSuffix;
2005-07-01 wenzelm 2005-07-01 added profiler interface, keep 'profiling' of PolyML structure; removed PolyML.Compiler.printInAlphabeticalOrder := false;
2005-06-21 wenzelm 2005-06-21 tuned pointer_eq;
2005-06-20 wenzelm 2005-06-20 added pointer_eq;
2005-06-17 wenzelm 2005-06-17 PolyML.Compiler.printInAlphabeticalOrder := false;
2005-06-11 wenzelm 2005-06-11 some cygwin support;
2005-06-05 wenzelm 2005-06-05 removed file_info (now in Pure/General/file.ML);
2005-04-26 wenzelm 2005-04-26 eval command line: show results; tuned;
2005-04-23 wenzelm 2005-04-23 eval command line arguments; tuned;
2005-04-13 paulson 2005-04-13 new signalling primmitives for sml/nj compatibility
2005-04-12 paulson 2005-04-12 fixing an incompatibility with Posix.IO.mkTextReader
2004-07-09 paulson 2004-07-09 new profiling function
2004-06-05 wenzelm 2004-06-05 tuned comments;
2004-06-01 webertj 2004-06-01 including polyml-time-limit.ML
2004-04-05 skalberg 2004-04-05 Added support for the newer versions of SML/NJ, which break several of the old interfaces.
2002-02-28 wenzelm 2002-02-28 renamed mask_interrupt to ignore_interrupt; renamed exhibit_interrupt to raise_interrupt; tuned interrupt handling code;
2001-11-08 wenzelm 2001-11-08 removed needs_filtered_use;
2001-02-06 wenzelm 2001-02-06 4.0 version;
2001-01-16 wenzelm 2001-01-16 use_text etc.: proper output of error messages;
2000-05-08 wenzelm 2000-05-08 val needs_filtered_use = true;
1999-10-20 wenzelm 1999-10-20 use_text: remove last char from output;
1999-10-13 wenzelm 1999-10-13 system; use_text: pass print function;
1999-08-02 wenzelm 1999-08-02 removed obsolete concat;
1999-08-02 paulson 1999-08-02 String.isPrefix
1999-07-28 paulson 1999-07-28 added String.concat
1999-02-04 wenzelm 1999-02-04 fixed file_info;
1998-12-28 paulson 1998-12-28 Basis Library compatible substring oeration
1998-11-09 wenzelm 1998-11-09 fake interrupt handler;
1998-06-29 wenzelm 1998-06-29 use_text: verbose flag;