more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
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