2007-09-16 wenzelm 2007-09-16 use_text/file: tune text (cf. ML_Parse.fix_ints);
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-29 wenzelm 2006-12-29 use_ml: reverted to simple output (Poly/ML changed);
2006-12-14 wenzelm 2006-12-14 activated improved use_ml, which captures output and reports source positions; define use_file in terms of use_ml;
2006-12-11 wenzelm 2006-12-11 added improved versions of use_text/file (still inactive);
2006-12-05 wenzelm 2006-12-05 setup for polyml-5.0;