src/Pure/ML-Systems/smlnj.ML
changeset 23965 f93e509659c1
parent 23921 947152add153
child 24145 c6402b61d44a
--- a/src/Pure/ML-Systems/smlnj.ML	Tue Jul 24 19:44:36 2007 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Tue Jul 24 19:44:37 2007 +0200
@@ -4,7 +4,8 @@
 Compatibility file for Standard ML of New Jersey 110 or later.
 *)
 
-use "ML-Systems/no_multithreading.ML";
+use "ML-Systems/exn.ML";
+use "ML-Systems/multithreading_dummy.ML";
 
 
 (** ML system related **)
@@ -127,37 +128,26 @@
 
 exception Interrupt;
 
-local
-
-fun capture f x = ((f x): unit; NONE) handle exn => SOME exn;
-
-fun release NONE = ()
-  | release (SOME exn) = raise exn;
-
-in
-
 fun ignore_interrupt f x =
   let
     val old_handler = Signals.setHandler (Signals.sigINT, Signals.IGNORE);
-    val result = capture f x;
+    val result = Exn.capture f x;
     val _ = Signals.setHandler (Signals.sigINT, old_handler);
-  in release result end;
+  in Exn.release result end;
 
 fun raise_interrupt f x =
   let
     val interrupted = ref false;
-    val result = ref NONE;
+    val result = ref (Exn.Result ());
     val old_handler = Signals.inqHandler Signals.sigINT;
   in
     SMLofNJ.Cont.callcc (fn cont =>
       (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => (interrupted := true; cont)));
-      result := capture f x));
+      result := Exn.capture f x));
     Signals.setHandler (Signals.sigINT, old_handler);
-    if ! interrupted then raise Interrupt else release (! result)
+    if ! interrupted then raise Interrupt else Exn.release (! result)
   end;
 
-end;
-
 
 (* basis library fixes *)