ML-Systems/exn.ML, ML-Systems/multithreading_dummy.ML;
authorwenzelm
Tue Jul 24 19:44:37 2007 +0200 (2007-07-24)
changeset 23965f93e509659c1
parent 23964 d2df2797519b
child 23966 25f34ff5eedf
ML-Systems/exn.ML, ML-Systems/multithreading_dummy.ML;
src/Pure/ML-Systems/alice.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/Pure/ML-Systems/alice.ML	Tue Jul 24 19:44:36 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/alice.ML	Tue Jul 24 19:44:37 2007 +0200
     1.3 @@ -13,7 +13,8 @@
     1.4  - Session.finish ();
     1.5  *)
     1.6  
     1.7 -use "ML-Systems/no_multithreading.ML";
     1.8 +use "ML-Systems/exn.ML";
     1.9 +use "ML-Systems/multithreading_dummy.ML";
    1.10  
    1.11  
    1.12  fun exit 0 = (OS.Process.exit OS.Process.success): unit
     2.1 --- a/src/Pure/ML-Systems/mosml.ML	Tue Jul 24 19:44:36 2007 +0200
     2.2 +++ b/src/Pure/ML-Systems/mosml.ML	Tue Jul 24 19:44:37 2007 +0200
     2.3 @@ -29,7 +29,8 @@
     2.4  load "FileSys";
     2.5  load "IO";
     2.6  
     2.7 -use "ML-Systems/no_multithreading.ML";
     2.8 +use "ML-Systems/exn.ML";
     2.9 +use "ML-Systems/multithreading_dummy.ML";
    2.10  
    2.11  
    2.12  (*low-level pointer equality*)
     3.1 --- a/src/Pure/ML-Systems/polyml.ML	Tue Jul 24 19:44:36 2007 +0200
     3.2 +++ b/src/Pure/ML-Systems/polyml.ML	Tue Jul 24 19:44:37 2007 +0200
     3.3 @@ -4,7 +4,8 @@
     3.4  Compatibility file for Poly/ML (version 4.1.x and 4.2.0).
     3.5  *)
     3.6  
     3.7 -use "ML-Systems/no_multithreading.ML";
     3.8 +use "ML-Systems/exn.ML";
     3.9 +use "ML-Systems/multithreading_dummy.ML";
    3.10  
    3.11  
    3.12  (** ML system and platform related **)
    3.13 @@ -121,20 +122,15 @@
    3.14  
    3.15  local
    3.16  
    3.17 -fun capture f x = ((f x): unit; NONE) handle exn => SOME exn;
    3.18 -
    3.19 -fun release NONE = ()
    3.20 -  | release (SOME exn) = raise exn;
    3.21 -
    3.22  val sig_int = 2;
    3.23  
    3.24  fun change_signal new_handler f x =
    3.25    let
    3.26      (*RACE wrt. other signals*)
    3.27      val old_handler = Signal.signal (sig_int, new_handler);
    3.28 -    val result = capture f x;
    3.29 +    val result = Exn.capture f x;
    3.30      val _ = Signal.signal (sig_int, old_handler);
    3.31 -  in release result end;
    3.32 +  in Exn.release result end;
    3.33  
    3.34  val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
    3.35  
     4.1 --- a/src/Pure/ML-Systems/smlnj.ML	Tue Jul 24 19:44:36 2007 +0200
     4.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Tue Jul 24 19:44:37 2007 +0200
     4.3 @@ -4,7 +4,8 @@
     4.4  Compatibility file for Standard ML of New Jersey 110 or later.
     4.5  *)
     4.6  
     4.7 -use "ML-Systems/no_multithreading.ML";
     4.8 +use "ML-Systems/exn.ML";
     4.9 +use "ML-Systems/multithreading_dummy.ML";
    4.10  
    4.11  
    4.12  (** ML system related **)
    4.13 @@ -127,37 +128,26 @@
    4.14  
    4.15  exception Interrupt;
    4.16  
    4.17 -local
    4.18 -
    4.19 -fun capture f x = ((f x): unit; NONE) handle exn => SOME exn;
    4.20 -
    4.21 -fun release NONE = ()
    4.22 -  | release (SOME exn) = raise exn;
    4.23 -
    4.24 -in
    4.25 -
    4.26  fun ignore_interrupt f x =
    4.27    let
    4.28      val old_handler = Signals.setHandler (Signals.sigINT, Signals.IGNORE);
    4.29 -    val result = capture f x;
    4.30 +    val result = Exn.capture f x;
    4.31      val _ = Signals.setHandler (Signals.sigINT, old_handler);
    4.32 -  in release result end;
    4.33 +  in Exn.release result end;
    4.34  
    4.35  fun raise_interrupt f x =
    4.36    let
    4.37      val interrupted = ref false;
    4.38 -    val result = ref NONE;
    4.39 +    val result = ref (Exn.Result ());
    4.40      val old_handler = Signals.inqHandler Signals.sigINT;
    4.41    in
    4.42      SMLofNJ.Cont.callcc (fn cont =>
    4.43        (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => (interrupted := true; cont)));
    4.44 -      result := capture f x));
    4.45 +      result := Exn.capture f x));
    4.46      Signals.setHandler (Signals.sigINT, old_handler);
    4.47 -    if ! interrupted then raise Interrupt else release (! result)
    4.48 +    if ! interrupted then raise Interrupt else Exn.release (! result)
    4.49    end;
    4.50  
    4.51 -end;
    4.52 -
    4.53  
    4.54  (* basis library fixes *)
    4.55