more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
authorwenzelm
Fri, 19 Aug 2011 13:32:27 +0200
changeset 451710c4411e2fc90
parent 45170 e43f0ea90c9a
child 45172 b3bd26fd22d3
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
src/Pure/Concurrent/par_exn.ML
     1.1 --- a/src/Pure/Concurrent/par_exn.ML	Fri Aug 19 12:51:14 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/par_exn.ML	Fri Aug 19 13:32:27 2011 +0200
     1.3 @@ -22,7 +22,11 @@
     1.4  fun serial exn =
     1.5    (case get_exn_serial exn of
     1.6      SOME i => (i, exn)
     1.7 -  | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
     1.8 +  | NONE =>
     1.9 +      let
    1.10 +        val i = Library.serial ();
    1.11 +        val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
    1.12 +      in (i, exn') end);
    1.13  
    1.14  val the_serial = the o get_exn_serial;
    1.15