src/Pure/ML-Systems/polyml.ML
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;
1998-06-15 wenzelm 1998-06-15 use_text replaces use_strings;
1998-05-28 wenzelm 1998-05-28 fixed ml_prompts;
1998-05-28 wenzelm 1998-05-28 added ml_prompts;
1997-12-17 wenzelm 1997-12-17 tuned comment;
1997-11-28 paulson 1997-11-28 New timing functions startTiming and endTiming
1997-08-06 wenzelm 1997-08-06 renamed use_string to use_strings;
1997-08-05 wenzelm 1997-08-05 cleaned up; added getenv;
1996-12-16 wenzelm 1996-12-16 added needs_filtered_use;
1996-12-09 wenzelm 1996-12-09 Compatibility file for Poly/ML (versions 2.x, 3.x).