# HG changeset patch # User skalberg # Date 1081164190 -7200 # Node ID 4ca3608fdf4f5492386fad20f9ef7dc66f5e39b9 # Parent c3019a66180f2b5016b645b3811ad903f687215a Added support for the newer versions of SML/NJ, which break several of the old interfaces. diff -r c3019a66180f -r 4ca3608fdf4f src/Pure/IsaMakefile --- 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 \ diff -r c3019a66180f -r 4ca3608fdf4f src/Pure/ML-Systems/cpu-timer-basis.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; + diff -r c3019a66180f -r 4ca3608fdf4f src/Pure/ML-Systems/cpu-timer-gc.ML --- /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; + diff -r c3019a66180f -r 4ca3608fdf4f src/Pure/ML-Systems/mlworks.ML --- 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 *) diff -r c3019a66180f -r 4ca3608fdf4f src/Pure/ML-Systems/mosml.ML --- 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 *) diff -r c3019a66180f -r 4ca3608fdf4f src/Pure/ML-Systems/polyml.ML --- 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 *) diff -r c3019a66180f -r 4ca3608fdf4f src/Pure/ML-Systems/smlnj-basis-compat.ML --- /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 diff -r c3019a66180f -r 4ca3608fdf4f src/Pure/ML-Systems/smlnj-pp-new.ML --- /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; diff -r c3019a66180f -r 4ca3608fdf4f src/Pure/ML-Systems/smlnj-pp-old.ML --- /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; diff -r c3019a66180f -r 4ca3608fdf4f src/Pure/ML-Systems/smlnj.ML --- 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;