--- a/src/Pure/IsaMakefile Fri Nov 10 23:22:03 2006 +0100
+++ b/src/Pure/IsaMakefile Fri Nov 10 23:22:04 2006 +0100
@@ -42,13 +42,9 @@
Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML \
Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML Isar/specification.ML \
Isar/term_style.ML Isar/theory_target.ML Isar/thy_header.ML Isar/toplevel.ML \
- ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML \
ML-Systems/polyml-4.1.4-patch.ML ML-Systems/polyml-4.2.0.ML \
ML-Systems/polyml-4.9.1.ML ML-Systems/polyml-interrupt-timeout.ML \
ML-Systems/polyml-posix.ML ML-Systems/polyml.ML ML-Systems/poplogml.ML \
- ML-Systems/smlnj-basis-compat.ML ML-Systems/smlnj-compiler.ML \
- ML-Systems/smlnj-interrupt-timeout.ML ML-Systems/smlnj-pp-new.ML \
- ML-Systems/smlnj-pp-old.ML ML-Systems/smlnj-ptreql.ML \
ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML \
Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
Pure.thy ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML \
--- a/src/Pure/ML-Systems/cpu-timer-basis.ML Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* 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;
-
-fun checkTimer timer =
- let
- val {sys, usr} = Timer.checkCPUTimer timer;
- val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *)
- in (sys, usr, gc) end;
--- a/src/Pure/ML-Systems/cpu-timer-gc.ML Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* 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;
-
-fun checkTimer timer =
- let val {sys, usr, gc} = Timer.checkCPUTimer timer
- in (sys, usr, gc) end;
--- a/src/Pure/ML-Systems/smlnj-basis-compat.ML Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: Pure/ML-Systems/smlnj-basis-compat.ML
- ID: $Id$
- Author: Sebastian Skalberg (TU Muenchen)
-
-Compatibility file for Standard ML of New Jersey 110.44 or later. Here
-signatures that have changed to adhere to the SML Basis Library are
-changed back to their old values.
-*)
-
-structure TextIO =
-struct
- open TextIO;
-
- fun inputLine is =
- (case TextIO.inputLine is of
- SOME str => str
- | NONE => "")
- handle IO.Io _ => raise Interrupt;
-end;
--- a/src/Pure/ML-Systems/smlnj-compiler.ML Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: Pure/ML-Systems/smlnj.ML
- ID: $Id$
- Author: Markus Wenzel, LMU Muenchen
-
-Compatibility tweak for later versions of Standard ML of New Jersey 110.
-*)
-
-structure Compiler =
-struct
- open Compiler;
- structure Control = Control;
- structure PrettyPrint = PrettyPrint;
- structure PPTable = CompilerPPTable;
- structure Interact = Backend.Interact;
-end;
--- a/src/Pure/ML-Systems/smlnj-interrupt-timeout.ML Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(* Title: Pure/ML-Systems/smlnj-interrupt-timeout.ML
- ID: $Id$
- Author: Tjark Weber, Makarius
- Copyright 2006
-
-Bounded time execution (similar to SML/NJ's TimeLimit structure).
-*)
-
-fun interrupt_timeout time f x =
- TimeLimit.timeLimit time f x
- handle TimeLimit.TimeOut => raise Interrupt;
--- a/src/Pure/ML-Systems/smlnj-pp-new.ML Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* 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;
--- a/src/Pure/ML-Systems/smlnj-pp-old.ML Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* 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-ptreql.ML Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-(* Title: $Id$
- Author: Lawrence C Paulson
-
-Pointer Equality: for Standard ML of New Jersey 110.49 or later.
-
-Thanks to Matthias Blume for providing InlineT.ptreql!
-*)
-
-CM.autoload "$smlnj/init/init.cmi";
-val pointer_eq = InlineT.ptreql;