moved exception capture/release to structure Exn;
authorwenzelm
Tue Jul 24 19:44:38 2007 +0200 (2007-07-24)
changeset 2396625f34ff5eedf
parent 23965 f93e509659c1
child 23967 92130b24e87f
moved exception capture/release to structure Exn;
moved multithreading to multithreading_polyml.ML;
src/Pure/ML-Systems/polyml-5.1.ML
     1.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Jul 24 19:44:37 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Jul 24 19:44:38 2007 +0200
     1.3 @@ -5,6 +5,7 @@
     1.4  *)
     1.5  
     1.6  use "ML-Systems/polyml.ML";
     1.7 +use "ML-Systems/multithreading_polyml.ML";
     1.8  
     1.9  val pointer_eq = PolyML.pointerEq;
    1.10  
    1.11 @@ -39,54 +40,3 @@
    1.12      val instream = TextIO.openIn name;
    1.13      val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    1.14    in use_text name output verbose txt end;
    1.15 -
    1.16 -
    1.17 -
    1.18 -(** multithreading **)
    1.19 -
    1.20 -open Thread;
    1.21 -
    1.22 -local
    1.23 -
    1.24 -datatype 'a result =
    1.25 -  Result of 'a |
    1.26 -  Exn of exn;
    1.27 -
    1.28 -fun capture f x = Result (f x) handle e => Exn e;
    1.29 -
    1.30 -fun release (Result y) = y
    1.31 -  | release (Exn e) = raise e;
    1.32 -
    1.33 -fun message s =
    1.34 -  (TextIO.output (TextIO.stdErr, (">>> " ^ s ^ "\n")); TextIO.flushOut TextIO.stdErr);
    1.35 -
    1.36 -
    1.37 -val critical_lock = Mutex.mutex ();
    1.38 -val critical_thread = ref (NONE: Thread.thread option);
    1.39 -
    1.40 -in
    1.41 -
    1.42 -(* critical section -- may be nested within the same thread *)
    1.43 -
    1.44 -fun self_critical () =
    1.45 -  (case ! critical_thread of
    1.46 -    NONE => false
    1.47 -  | SOME id => Thread.equal (id, Thread.self ()));
    1.48 -
    1.49 -fun CRITICAL e =
    1.50 -  if self_critical () then e ()
    1.51 -  else
    1.52 -    let
    1.53 -      val _ =
    1.54 -        if Mutex.trylock critical_lock then ()
    1.55 -        else
    1.56 -          (message "Waiting for critical lock";
    1.57 -           Mutex.lock critical_lock;
    1.58 -           message "Obtained critical lock");
    1.59 -      val _ = critical_thread := SOME (Thread.self ());
    1.60 -      val res = capture e ();
    1.61 -      val _ = critical_thread := NONE;
    1.62 -      val _ = Mutex.unlock critical_lock;
    1.63 -    in release res end;
    1.64 -
    1.65 -end;