# HG changeset patch
# User wenzelm
# Date 1185299077 -7200
# Node ID f93e509659c1c0711427e91af1cbe923b59aa1bc
# Parent  d2df2797519bcb78204c47637f25344f612d5ad2
ML-Systems/exn.ML, ML-Systems/multithreading_dummy.ML;

diff -r d2df2797519b -r f93e509659c1 src/Pure/ML-Systems/alice.ML
--- a/src/Pure/ML-Systems/alice.ML	Tue Jul 24 19:44:36 2007 +0200
+++ b/src/Pure/ML-Systems/alice.ML	Tue Jul 24 19:44:37 2007 +0200
@@ -13,7 +13,8 @@
 - Session.finish ();
 *)
 
-use "ML-Systems/no_multithreading.ML";
+use "ML-Systems/exn.ML";
+use "ML-Systems/multithreading_dummy.ML";
 
 
 fun exit 0 = (OS.Process.exit OS.Process.success): unit
diff -r d2df2797519b -r f93e509659c1 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Tue Jul 24 19:44:36 2007 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Tue Jul 24 19:44:37 2007 +0200
@@ -29,7 +29,8 @@
 load "FileSys";
 load "IO";
 
-use "ML-Systems/no_multithreading.ML";
+use "ML-Systems/exn.ML";
+use "ML-Systems/multithreading_dummy.ML";
 
 
 (*low-level pointer equality*)
diff -r d2df2797519b -r f93e509659c1 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Jul 24 19:44:36 2007 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Jul 24 19:44:37 2007 +0200
@@ -4,7 +4,8 @@
 Compatibility file for Poly/ML (version 4.1.x and 4.2.0).
 *)
 
-use "ML-Systems/no_multithreading.ML";
+use "ML-Systems/exn.ML";
+use "ML-Systems/multithreading_dummy.ML";
 
 
 (** ML system and platform related **)
@@ -121,20 +122,15 @@
 
 local
 
-fun capture f x = ((f x): unit; NONE) handle exn => SOME exn;
-
-fun release NONE = ()
-  | release (SOME exn) = raise exn;
-
 val sig_int = 2;
 
 fun change_signal new_handler f x =
   let
     (*RACE wrt. other signals*)
     val old_handler = Signal.signal (sig_int, new_handler);
-    val result = capture f x;
+    val result = Exn.capture f x;
     val _ = Signal.signal (sig_int, old_handler);
-  in release result end;
+  in Exn.release result end;
 
 val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
 
diff -r d2df2797519b -r f93e509659c1 src/Pure/ML-Systems/smlnj.ML
--- 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 *)