# HG changeset patch
# User wenzelm
# Date 1243780912 -7200
# Node ID 6974449ddea96eb46548a14a262beafb49af542d
# Parent  133d1cfd6ae70cd6d0efb219d5a69623a9e0058d
no longer open PolyML -- to avoid surprises within the global name space;
recovered some important PolyML bindings (NB: print and makestring cannot be rebound without loosing infinite overloading);

diff -r 133d1cfd6ae7 -r 6974449ddea9 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Sun May 31 16:29:39 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sun May 31 16:41:52 2009 +0200
@@ -28,13 +28,7 @@
 
 (* old Poly/ML emulation *)
 
-local
-  val orig_exit = exit;
-in
-  open PolyML;
-  val exit = orig_exit;
-  fun quit () = exit 0;
-end;
+fun quit () = exit 0;
 
 
 (* restore old-style character / string functions *)
@@ -83,6 +77,8 @@
   fun print_depth n = (depth := n; PolyML.print_depth n);
 end;
 
+val error_depth = PolyML.error_depth;
+
 
 
 (** interrupts **)
@@ -134,7 +130,12 @@
   | SOME txt => txt);
 
 
-(* profile execution *)
+
+(** Runtime system **)
+
+val exception_trace = PolyML.exception_trace;
+val timing = PolyML.timing;
+val profiling = PolyML.profiling;
 
 fun profile 0 f x = f x
   | profile n f x =