interrupt_timeout now raises Interrupt instead of SML90.Interrupt
authorwebertj
Thu, 26 Jan 2006 20:42:15 +0100
changeset 18790 418131f631fc
parent 18789 8a5c6fc3ad27
child 18791 9b4ae9fa67a4
interrupt_timeout now raises Interrupt instead of SML90.Interrupt
src/Pure/ML-Systems/smlnj-interrupt-timeout.ML
src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj-interrupt-timeout.ML	Thu Jan 26 20:17:54 2006 +0100
+++ b/src/Pure/ML-Systems/smlnj-interrupt-timeout.ML	Thu Jan 26 20:42:15 2006 +0100
@@ -8,4 +8,4 @@
 
 fun interrupt_timeout time f x =
   TimeLimit.timeLimit time f x
-    handle TimeLimit.TimeOut => raise SML90.Interrupt;
+    handle TimeLimit.TimeOut => raise Interrupt;
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Jan 26 20:17:54 2006 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Jan 26 20:42:15 2006 +0100
@@ -59,11 +59,6 @@
 | _ => use "ML-Systems/cpu-timer-gc.ML");
 
 
-(* bounded time execution *)
-
-use "ML-Systems/smlnj-interrupt-timeout.ML";
-
-
 (*prompts*)
 fun ml_prompts p1 p2 =
   (Compiler.Control.primaryPrompt := p1; Compiler.Control.secondaryPrompt := p2);
@@ -108,7 +103,6 @@
   end;
 
 
-
 (** interrupts **)
 
 exception Interrupt;
@@ -151,6 +145,12 @@
 | _ => ());
 
 
+
+(* bounded time execution *)
+
+use "ML-Systems/smlnj-interrupt-timeout.ML";
+
+
 (** Signal handling: emulation of the Poly/ML Signal structure. Note that types
     Posix.Signal.signal and Signals.signal differ **)