more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
authorwenzelm
Fri, 19 Aug 2011 13:32:27 +0200
changeset 44296 0c4411e2fc90
parent 44295 e43f0ea90c9a
child 44297 b3bd26fd22d3
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Fri Aug 19 12:51:14 2011 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Fri Aug 19 13:32:27 2011 +0200
@@ -22,7 +22,11 @@
 fun serial exn =
   (case get_exn_serial exn of
     SOME i => (i, exn)
-  | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
+  | NONE =>
+      let
+        val i = Library.serial ();
+        val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
+      in (i, exn') end);
 
 val the_serial = the o get_exn_serial;