Added support for the newer versions of SML/NJ, which break several of the
old interfaces.
--- a/src/Pure/IsaMakefile Sun Apr 04 15:34:14 2004 +0200
+++ b/src/Pure/IsaMakefile Mon Apr 05 13:23:10 2004 +0200
@@ -41,8 +41,10 @@
Isar/thy_header.ML Isar/toplevel.ML ML-Systems/mlworks.ML \
ML-Systems/polyml-3.x.ML ML-Systems/polyml.ML \
ML-Systems/smlnj-0.93.ML ML-Systems/smlnj-compiler.ML \
- ML-Systems/smlnj.ML Proof/ROOT.ML Proof/extraction.ML \
- Proof/proof_rewrite_rules.ML \
+ ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML \
+ ML-Systems/smlnj-pp-new.ML ML-Systems/smlnj-pp-old.ML \
+ ML-Systems/smlnj.ML ML-Systems/smlnj-basis-compat.ML Proof/ROOT.ML \
+ Proof/extraction.ML Proof/proof_rewrite_rules.ML \
Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML \
Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/cpu-timer-basis.ML Mon Apr 05 13:23:10 2004 +0200
@@ -0,0 +1,23 @@
+(* Title: Pure/ML-Systems/cpu-timer-basis.ML
+ ID: $Id$
+ Author: Sebastian Skalberg (TU Muenchen)
+
+Implementation of timing functions, building on standard ("basis library") functions.
+*)
+
+(*Note start point for timing*)
+fun startTiming() =
+ let val CPUtimer = Timer.startCPUTimer();
+ val time = Timer.checkCPUTimer(CPUtimer)
+ in (CPUtimer,time) end;
+
+(*Finish timing and return string*)
+fun endTiming (CPUtimer, {sys,usr}) =
+ let open Time (*...for Time.toString, Time.+ and Time.- *)
+ val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
+ in "User " ^ toString (usr2-usr) ^
+ " All "^ toString (sys2-sys + usr2-usr) ^
+ " secs"
+ handle Time => ""
+ end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/cpu-timer-gc.ML Mon Apr 05 13:23:10 2004 +0200
@@ -0,0 +1,25 @@
+(* Title: Pure/ML-Systems/cpu-timer-gc.ML
+ ID: $Id$
+ Author: Sebastian Skalberg (TU Muenchen)
+
+Implementation of timing functions, building on implementations where
+the return type of Timer.checkCPUTimer includes a gc field.
+*)
+
+(*Note start point for timing*)
+fun startTiming() =
+ let val CPUtimer = Timer.startCPUTimer();
+ val time = Timer.checkCPUTimer(CPUtimer)
+ in (CPUtimer,time) end;
+
+(*Finish timing and return string*)
+fun endTiming (CPUtimer, {gc,sys,usr}) =
+ let open Time (*...for Time.toString, Time.+ and Time.- *)
+ val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
+ in "User " ^ toString (usr2-usr) ^
+ " GC " ^ toString (gc2-gc) ^
+ " All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
+ " secs"
+ handle Time => ""
+ end;
+
--- a/src/Pure/ML-Systems/mlworks.ML Sun Apr 04 15:34:14 2004 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML Mon Apr 05 13:23:10 2004 +0200
@@ -57,22 +57,7 @@
(** Compiler-independent timing functions **)
-(*Note start point for timing*)
-fun startTiming() =
- let val CPUtimer = Timer.startCPUTimer();
- val time = Timer.checkCPUTimer(CPUtimer)
- in (CPUtimer,time) end;
-
-(*Finish timing and return string*)
-fun endTiming (CPUtimer, {gc,sys,usr}) =
- let open Time (*...for Time.toString, Time.+ and Time.- *)
- val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
- in "User " ^ toString (usr2-usr) ^
- " GC " ^ toString (gc2-gc) ^
- " All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
- " secs"
- handle Time => ""
- end;
+use "ML-Systems/cpu-timer-gc.ML"
(* ML command execution *)
--- a/src/Pure/ML-Systems/mosml.ML Sun Apr 04 15:34:14 2004 +0200
+++ b/src/Pure/ML-Systems/mosml.ML Mon Apr 05 13:23:10 2004 +0200
@@ -58,22 +58,7 @@
load "Timer";
-(*Note start point for timing*)
-fun startTiming() =
- let val CPUtimer = Timer.startCPUTimer();
- val time = Timer.checkCPUTimer(CPUtimer)
- in (CPUtimer,time) end;
-
-(*Finish timing and return string*)
-fun endTiming (CPUtimer, {gc,sys,usr}) =
- let open Time (*...for Time.toString, Time.+ and Time.- *)
- val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
- in "User " ^ toString (usr2-usr) ^
- " GC " ^ toString (gc2-gc) ^
- " All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
- " secs"
- handle Time => ""
- end;
+use "ML-Systems/cpu-timer-gc.ML";
(* ML command execution *)
--- a/src/Pure/ML-Systems/polyml.ML Sun Apr 04 15:34:14 2004 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Mon Apr 05 13:23:10 2004 +0200
@@ -26,23 +26,9 @@
val explode = SML90.explode;
val implode = SML90.implode;
-
-(*Note start point for timing*)
-fun startTiming() =
- let val CPUtimer = Timer.startCPUTimer();
- val time = Timer.checkCPUTimer(CPUtimer)
- in (CPUtimer,time) end;
+(* compiler-independent timing functions *)
-(*Finish timing and return string*)
-fun endTiming (CPUtimer, {sys,usr}) =
- let open Time (*...for Time.toString, Time.+ and Time.- *)
- val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
- in "User " ^ toString (usr2-usr) ^
- " All "^ toString (sys2-sys + usr2-usr) ^
- " secs"
- handle Time => ""
- end;
-
+use "ML-Systems/cpu-timer-basis.ML";
(* prompts *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/smlnj-basis-compat.ML Mon Apr 05 13:23:10 2004 +0200
@@ -0,0 +1,17 @@
+(* Title: Pure/ML-Systems/smlnj-basis-compat.ML
+ ID: $Id$
+ Author: Sebastian Skalberg (TU Muenchen)
+
+Compatibility file for Standard ML of New Jersey 110.45 or later. Here
+signatures that have changed to adhere to the SML Basis Library are
+changed back to their old values. So much for standards...
+*)
+
+structure TextIO =
+struct
+open TextIO
+fun inputLine is =
+ case TextIO.inputLine is of
+ SOME str => str
+ | NONE => ""
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/smlnj-pp-new.ML Mon Apr 05 13:23:10 2004 +0200
@@ -0,0 +1,20 @@
+(* Title: Pure/ML-Systems/smlnj-pp-new.ML
+ ID: $Id$
+ Author: Sebastian Skalberg (TU Muenchen)
+
+Installation of the pretty printer, using SML/NJ's new pretty printer
+interface.
+*)
+
+fun make_pp path pprint =
+ let
+ open Compiler.PrettyPrint;
+
+ fun pp pps obj =
+ pprint obj
+ (string pps, openHOVBox pps o Rel,
+ fn wd => break pps {nsp=wd, offset=0}, fn () => newline pps,
+ fn () => closeBox pps);
+ in
+ (path, pp)
+ end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/smlnj-pp-old.ML Mon Apr 05 13:23:10 2004 +0200
@@ -0,0 +1,20 @@
+(* Title: Pure/ML-Systems/smlnj-pp-old.ML
+ ID: $Id$
+ Author: Sebastian Skalberg (TU Muenchen)
+
+Installation of the pretty printer, using SML/NJ's old pretty printer
+interface.
+*)
+
+fun make_pp path pprint =
+ let
+ open Compiler.PrettyPrint;
+
+ fun pp pps obj =
+ pprint obj
+ (add_string pps, begin_block pps INCONSISTENT,
+ fn wd => add_break pps (wd, 0), fn () => add_newline pps,
+ fn () => end_block pps);
+ in
+ (path, pp)
+ end;
--- a/src/Pure/ML-Systems/smlnj.ML Sun Apr 04 15:34:14 2004 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Mon Apr 05 13:23:10 2004 +0200
@@ -10,7 +10,6 @@
[110, x] => if x >= 35 then use "ML-Systems/smlnj-compiler.ML" else ()
| _ => ());
-
(** ML system related **)
(* restore old-style character / string functions *)
@@ -43,22 +42,11 @@
(* compiler-independent timing functions *)
-(*Note start point for timing*)
-fun startTiming() =
- let val CPUtimer = Timer.startCPUTimer();
- val time = Timer.checkCPUTimer(CPUtimer)
- in (CPUtimer,time) end;
-
-(*Finish timing and return string*)
-fun endTiming (CPUtimer, {gc,sys,usr}) =
- let open Time (*...for Time.toString, Time.+ and Time.- *)
- val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
- in "User " ^ toString (usr2-usr) ^
- " GC " ^ toString (gc2-gc) ^
- " All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
- " secs"
- handle Time => ""
- end;
+(case #version_id (Compiler.version) of
+ [110, x] => if x >= 45
+ then use "ML-Systems/cpu-timer-basis.ML"
+ else use "ML-Systems/cpu-timer-gc.ML"
+| _ => ());
(* prompts *)
@@ -67,20 +55,19 @@
(Compiler.Control.primaryPrompt := p1; Compiler.Control.secondaryPrompt := p2);
+(case #version_id (Compiler.version) of
+ [110, x] => if x >= 45
+ then use "ML-Systems/smlnj-basis-compat.ML"
+ else ()
+| _ => ());
+
(* toplevel pretty printing (see also Pure/install_pp.ML) *)
-fun make_pp path pprint =
- let
- open Compiler.PrettyPrint;
-
- fun pp pps obj =
- pprint obj
- (add_string pps, begin_block pps INCONSISTENT,
- fn wd => add_break pps (wd, 0), fn () => add_newline pps,
- fn () => end_block pps);
- in
- (path, pp)
- end;
+(case #version_id (Compiler.version) of
+ [110, x] => if x >= 45
+ then use "ML-Systems/smlnj-pp-new.ML"
+ else use "ML-Systems/smlnj-pp-old.ML"
+| _ => ());
fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;