# HG changeset patch
# User wenzelm
# Date 1457182645 -3600
# Node ID b8efcc9edd7b5984d28e71b9909862a30440e3fa
# Parent  091fdc002a527fc109478c169f867f73423771e4
avoid accidental handling of interrupts;
interrupts have no properties;

diff -r 091fdc002a52 -r b8efcc9edd7b src/Pure/ML/exn_properties.ML
--- a/src/Pure/ML/exn_properties.ML	Sat Mar 05 13:53:08 2016 +0100
+++ b/src/Pure/ML/exn_properties.ML	Sat Mar 05 13:57:25 2016 +0100
@@ -46,24 +46,26 @@
   | SOME loc => props_of_location loc);
 
 fun update entries exn =
-  let
-    val loc =
-      the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
-        (PolyML.exceptionLocation exn);
-    val props = props_of_location loc;
-    val props' = fold Properties.put entries props;
-  in
-    if props = props' then exn
-    else
-      let
-        val loc' =
-          {file = YXML.string_of_body (XML.Encode.properties props'),
-            startLine = #startLine loc, endLine = #endLine loc,
-            startPosition = #startPosition loc, endPosition = #endPosition loc};
-      in
-        uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
-          handle exn' => exn'
-      end
-  end;
+  if Exn.is_interrupt exn then exn
+  else
+    let
+      val loc =
+        the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
+          (PolyML.exceptionLocation exn);
+      val props = props_of_location loc;
+      val props' = fold Properties.put entries props;
+    in
+      if props = props' then exn
+      else
+        let
+          val loc' =
+            {file = YXML.string_of_body (XML.Encode.properties props'),
+              startLine = #startLine loc, endLine = #endLine loc,
+              startPosition = #startPosition loc, endPosition = #endPosition loc};
+        in
+          uninterruptible (fn _ => fn () =>
+            PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
+        end
+    end;
 
 end;