Added support for the newer versions of SML/NJ, which break several of the
authorskalberg
Mon Apr 05 13:23:10 2004 +0200 (2004-04-05)
changeset 145194ca3608fdf4f
parent 14518 c3019a66180f
child 14520 af9d7fcf873e
Added support for the newer versions of SML/NJ, which break several of the
old interfaces.
src/Pure/IsaMakefile
src/Pure/ML-Systems/cpu-timer-basis.ML
src/Pure/ML-Systems/cpu-timer-gc.ML
src/Pure/ML-Systems/mlworks.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj-basis-compat.ML
src/Pure/ML-Systems/smlnj-pp-new.ML
src/Pure/ML-Systems/smlnj-pp-old.ML
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/Pure/IsaMakefile	Sun Apr 04 15:34:14 2004 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Mon Apr 05 13:23:10 2004 +0200
     1.3 @@ -41,8 +41,10 @@
     1.4    Isar/thy_header.ML Isar/toplevel.ML ML-Systems/mlworks.ML		  \
     1.5    ML-Systems/polyml-3.x.ML ML-Systems/polyml.ML				  \
     1.6    ML-Systems/smlnj-0.93.ML ML-Systems/smlnj-compiler.ML			  \
     1.7 -  ML-Systems/smlnj.ML Proof/ROOT.ML Proof/extraction.ML			  \
     1.8 -  Proof/proof_rewrite_rules.ML						  \
     1.9 +  ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML                \
    1.10 +  ML-Systems/smlnj-pp-new.ML ML-Systems/smlnj-pp-old.ML                   \
    1.11 +  ML-Systems/smlnj.ML ML-Systems/smlnj-basis-compat.ML Proof/ROOT.ML      \
    1.12 +  Proof/extraction.ML Proof/proof_rewrite_rules.ML			  \
    1.13    Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML	  \
    1.14    ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML		  \
    1.15    Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML			  \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML-Systems/cpu-timer-basis.ML	Mon Apr 05 13:23:10 2004 +0200
     2.3 @@ -0,0 +1,23 @@
     2.4 +(*  Title:      Pure/ML-Systems/cpu-timer-basis.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     2.7 +
     2.8 +Implementation of timing functions, building on standard ("basis library") functions.
     2.9 +*)
    2.10 +
    2.11 +(*Note start point for timing*)
    2.12 +fun startTiming() =
    2.13 +  let val CPUtimer = Timer.startCPUTimer();
    2.14 +      val time = Timer.checkCPUTimer(CPUtimer)
    2.15 +  in  (CPUtimer,time)  end;
    2.16 +
    2.17 +(*Finish timing and return string*)
    2.18 +fun endTiming (CPUtimer, {sys,usr}) =
    2.19 +  let open Time  (*...for Time.toString, Time.+ and Time.- *)
    2.20 +      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    2.21 +  in  "User " ^ toString (usr2-usr) ^
    2.22 +      "  All "^ toString (sys2-sys + usr2-usr) ^
    2.23 +      " secs"
    2.24 +      handle Time => ""
    2.25 +  end;
    2.26 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ML-Systems/cpu-timer-gc.ML	Mon Apr 05 13:23:10 2004 +0200
     3.3 @@ -0,0 +1,25 @@
     3.4 +(*  Title:      Pure/ML-Systems/cpu-timer-gc.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     3.7 +
     3.8 +Implementation of timing functions, building on implementations where
     3.9 +the return type of Timer.checkCPUTimer includes a gc field.
    3.10 +*)
    3.11 +
    3.12 +(*Note start point for timing*)
    3.13 +fun startTiming() =
    3.14 +  let val CPUtimer = Timer.startCPUTimer();
    3.15 +      val time = Timer.checkCPUTimer(CPUtimer)
    3.16 +  in  (CPUtimer,time)  end;
    3.17 +
    3.18 +(*Finish timing and return string*)
    3.19 +fun endTiming (CPUtimer, {gc,sys,usr}) =
    3.20 +  let open Time  (*...for Time.toString, Time.+ and Time.- *)
    3.21 +      val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    3.22 +  in  "User " ^ toString (usr2-usr) ^
    3.23 +      "  GC " ^ toString (gc2-gc) ^
    3.24 +      "  All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
    3.25 +      " secs"
    3.26 +      handle Time => ""
    3.27 +  end;
    3.28 +
     4.1 --- a/src/Pure/ML-Systems/mlworks.ML	Sun Apr 04 15:34:14 2004 +0200
     4.2 +++ b/src/Pure/ML-Systems/mlworks.ML	Mon Apr 05 13:23:10 2004 +0200
     4.3 @@ -57,22 +57,7 @@
     4.4  
     4.5  (** Compiler-independent timing functions **)
     4.6  
     4.7 -(*Note start point for timing*)
     4.8 -fun startTiming() = 
     4.9 -  let val CPUtimer = Timer.startCPUTimer();
    4.10 -      val time = Timer.checkCPUTimer(CPUtimer)
    4.11 -  in  (CPUtimer,time)  end;
    4.12 -
    4.13 -(*Finish timing and return string*)
    4.14 -fun endTiming (CPUtimer, {gc,sys,usr}) =
    4.15 -  let open Time  (*...for Time.toString, Time.+ and Time.- *)
    4.16 -      val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    4.17 -  in  "User " ^ toString (usr2-usr) ^
    4.18 -      "  GC " ^ toString (gc2-gc) ^
    4.19 -      "  All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
    4.20 -      " secs"
    4.21 -      handle Time => ""
    4.22 -  end;
    4.23 +use "ML-Systems/cpu-timer-gc.ML"
    4.24  
    4.25  
    4.26  (* ML command execution *)
     5.1 --- a/src/Pure/ML-Systems/mosml.ML	Sun Apr 04 15:34:14 2004 +0200
     5.2 +++ b/src/Pure/ML-Systems/mosml.ML	Mon Apr 05 13:23:10 2004 +0200
     5.3 @@ -58,22 +58,7 @@
     5.4  
     5.5  load "Timer";
     5.6  
     5.7 -(*Note start point for timing*)
     5.8 -fun startTiming() = 
     5.9 -  let val CPUtimer = Timer.startCPUTimer();
    5.10 -      val time = Timer.checkCPUTimer(CPUtimer)
    5.11 -  in  (CPUtimer,time)  end;
    5.12 -
    5.13 -(*Finish timing and return string*)
    5.14 -fun endTiming (CPUtimer, {gc,sys,usr}) =
    5.15 -  let open Time  (*...for Time.toString, Time.+ and Time.- *)
    5.16 -      val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    5.17 -  in  "User " ^ toString (usr2-usr) ^
    5.18 -      "  GC " ^ toString (gc2-gc) ^
    5.19 -      "  All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
    5.20 -      " secs"
    5.21 -      handle Time => ""
    5.22 -  end;
    5.23 +use "ML-Systems/cpu-timer-gc.ML";
    5.24  
    5.25  
    5.26  (* ML command execution *)
     6.1 --- a/src/Pure/ML-Systems/polyml.ML	Sun Apr 04 15:34:14 2004 +0200
     6.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Apr 05 13:23:10 2004 +0200
     6.3 @@ -26,23 +26,9 @@
     6.4  val explode = SML90.explode;
     6.5  val implode = SML90.implode;
     6.6  
     6.7 -
     6.8 -(*Note start point for timing*)
     6.9 -fun startTiming() =
    6.10 -  let val CPUtimer = Timer.startCPUTimer();
    6.11 -      val time = Timer.checkCPUTimer(CPUtimer)
    6.12 -  in  (CPUtimer,time)  end;
    6.13 +(* compiler-independent timing functions *)
    6.14  
    6.15 -(*Finish timing and return string*)
    6.16 -fun endTiming (CPUtimer, {sys,usr}) =
    6.17 -  let open Time  (*...for Time.toString, Time.+ and Time.- *)
    6.18 -      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    6.19 -  in  "User " ^ toString (usr2-usr) ^
    6.20 -      "  All "^ toString (sys2-sys + usr2-usr) ^
    6.21 -      " secs"
    6.22 -      handle Time => ""
    6.23 -  end;
    6.24 -
    6.25 +use "ML-Systems/cpu-timer-basis.ML";
    6.26  
    6.27  (* prompts *)
    6.28  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/ML-Systems/smlnj-basis-compat.ML	Mon Apr 05 13:23:10 2004 +0200
     7.3 @@ -0,0 +1,17 @@
     7.4 +(*  Title:      Pure/ML-Systems/smlnj-basis-compat.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     7.7 +
     7.8 +Compatibility file for Standard ML of New Jersey 110.45 or later. Here
     7.9 +signatures that have changed to adhere to the SML Basis Library are
    7.10 +changed back to their old values. So much for standards...
    7.11 +*)
    7.12 +
    7.13 +structure TextIO =
    7.14 +struct
    7.15 +open TextIO
    7.16 +fun inputLine is =
    7.17 +    case TextIO.inputLine is of
    7.18 +	SOME str => str
    7.19 +      | NONE => ""
    7.20 +end;
    7.21 \ No newline at end of file
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/ML-Systems/smlnj-pp-new.ML	Mon Apr 05 13:23:10 2004 +0200
     8.3 @@ -0,0 +1,20 @@
     8.4 +(*  Title:      Pure/ML-Systems/smlnj-pp-new.ML
     8.5 +    ID:         $Id$
     8.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     8.7 +
     8.8 +Installation of the pretty printer, using SML/NJ's new pretty printer
     8.9 +interface.
    8.10 +*)
    8.11 +
    8.12 +fun make_pp path pprint =
    8.13 +  let
    8.14 +    open Compiler.PrettyPrint;
    8.15 +
    8.16 +    fun pp pps obj =
    8.17 +      pprint obj
    8.18 +        (string pps, openHOVBox pps o Rel,
    8.19 +          fn wd => break pps {nsp=wd, offset=0}, fn () => newline pps,
    8.20 +          fn () => closeBox pps);
    8.21 +  in
    8.22 +    (path, pp)
    8.23 +  end;
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Pure/ML-Systems/smlnj-pp-old.ML	Mon Apr 05 13:23:10 2004 +0200
     9.3 @@ -0,0 +1,20 @@
     9.4 +(*  Title:      Pure/ML-Systems/smlnj-pp-old.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     9.7 +
     9.8 +Installation of the pretty printer, using SML/NJ's old pretty printer
     9.9 +interface.
    9.10 +*)
    9.11 +
    9.12 +fun make_pp path pprint =
    9.13 +  let
    9.14 +    open Compiler.PrettyPrint;
    9.15 +
    9.16 +    fun pp pps obj =
    9.17 +      pprint obj
    9.18 +        (add_string pps, begin_block pps INCONSISTENT,
    9.19 +          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
    9.20 +          fn () => end_block pps);
    9.21 +  in
    9.22 +    (path, pp)
    9.23 +  end;
    10.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sun Apr 04 15:34:14 2004 +0200
    10.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Apr 05 13:23:10 2004 +0200
    10.3 @@ -10,7 +10,6 @@
    10.4    [110, x] => if x >= 35 then use "ML-Systems/smlnj-compiler.ML" else ()
    10.5  | _ => ());
    10.6  
    10.7 -
    10.8  (** ML system related **)
    10.9  
   10.10  (* restore old-style character / string functions *)
   10.11 @@ -43,22 +42,11 @@
   10.12  
   10.13  (* compiler-independent timing functions *)
   10.14  
   10.15 -(*Note start point for timing*)
   10.16 -fun startTiming() =
   10.17 -  let val CPUtimer = Timer.startCPUTimer();
   10.18 -      val time = Timer.checkCPUTimer(CPUtimer)
   10.19 -  in  (CPUtimer,time)  end;
   10.20 -
   10.21 -(*Finish timing and return string*)
   10.22 -fun endTiming (CPUtimer, {gc,sys,usr}) =
   10.23 -  let open Time  (*...for Time.toString, Time.+ and Time.- *)
   10.24 -      val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
   10.25 -  in  "User " ^ toString (usr2-usr) ^
   10.26 -      "  GC " ^ toString (gc2-gc) ^
   10.27 -      "  All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
   10.28 -      " secs"
   10.29 -      handle Time => ""
   10.30 -  end;
   10.31 +(case #version_id (Compiler.version) of
   10.32 +  [110, x] => if x >= 45
   10.33 +	      then use "ML-Systems/cpu-timer-basis.ML"
   10.34 +	      else use "ML-Systems/cpu-timer-gc.ML"
   10.35 +| _ => ());
   10.36  
   10.37  
   10.38  (* prompts *)
   10.39 @@ -67,20 +55,19 @@
   10.40    (Compiler.Control.primaryPrompt := p1; Compiler.Control.secondaryPrompt := p2);
   10.41  
   10.42  
   10.43 +(case #version_id (Compiler.version) of
   10.44 +  [110, x] => if x >= 45
   10.45 +	      then use "ML-Systems/smlnj-basis-compat.ML"
   10.46 +	      else ()
   10.47 +| _ => ());
   10.48 +
   10.49  (* toplevel pretty printing (see also Pure/install_pp.ML) *)
   10.50  
   10.51 -fun make_pp path pprint =
   10.52 -  let
   10.53 -    open Compiler.PrettyPrint;
   10.54 -
   10.55 -    fun pp pps obj =
   10.56 -      pprint obj
   10.57 -        (add_string pps, begin_block pps INCONSISTENT,
   10.58 -          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
   10.59 -          fn () => end_block pps);
   10.60 -  in
   10.61 -    (path, pp)
   10.62 -  end;
   10.63 +(case #version_id (Compiler.version) of
   10.64 +  [110, x] => if x >= 45
   10.65 +	      then use "ML-Systems/smlnj-pp-new.ML"
   10.66 +	      else use "ML-Systems/smlnj-pp-old.ML"
   10.67 +| _ => ());
   10.68  
   10.69  fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;
   10.70