Sun, 07 Sep 2008 17:46:43 +0200 |
wenzelm |
explicit use of universal.ML and dummy_thread.ML;
|
file |
diff |
annotate
|
Mon, 24 Mar 2008 18:35:42 +0100 |
wenzelm |
moved use_text/file to polyml_old_compiler5.ML;
|
file |
diff |
annotate
|
Thu, 06 Mar 2008 19:21:26 +0100 |
wenzelm |
rearrangements to make latest Poly/ML the default, not old 4.x;
|
file |
diff |
annotate
|
Sun, 16 Sep 2007 20:25:43 +0200 |
wenzelm |
use_file: added ``tune'' argument;
|
file |
diff |
annotate
|
Sun, 16 Sep 2007 14:55:48 +0200 |
wenzelm |
use_text/file: tune text (cf. ML_Parse.fix_ints);
|
file |
diff |
annotate
|
Thu, 31 May 2007 01:25:24 +0200 |
wenzelm |
TextIO.inputLine: use present SML B library version;
|
file |
diff |
annotate
|
Sun, 21 Jan 2007 16:43:42 +0100 |
wenzelm |
use_text: added name argument;
|
file |
diff |
annotate
|
Fri, 29 Dec 2006 03:57:01 +0100 |
wenzelm |
use_ml: reverted to simple output (Poly/ML changed);
|
file |
diff |
annotate
|
Thu, 14 Dec 2006 21:46:59 +0100 |
wenzelm |
activated improved use_ml, which captures output and reports source positions;
|
file |
diff |
annotate
|
Mon, 11 Dec 2006 19:05:25 +0100 |
wenzelm |
added improved versions of use_text/file (still inactive);
|
file |
diff |
annotate
|
Tue, 05 Dec 2006 18:33:29 +0100 |
wenzelm |
setup for polyml-5.0;
|
file |
diff |
annotate
|