Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid handling interrupts in user code;
authorwenzelm
Thu, 09 Sep 2010 18:17:34 +0200
changeset 39236 2ec7afadc344
parent 39235 cda88e68106d
child 39237 be1acdcd55dc
avoid handling interrupts in user code;
src/HOL/Import/proof_kernel.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/proof_kernel.ML	Thu Sep 09 18:04:35 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Sep 09 18:17:34 2010 +0200
@@ -1299,10 +1299,13 @@
                     end
                   | NONE => (thy,NONE)
             end
-    end  (* FIXME avoid handle _ *)
+    end
     handle e =>
-      (if_debug (fn () => writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) ();
-        (thy,NONE))
+      if Exn.is_interrupt e then reraise e
+      else
+        (if_debug (fn () =>
+            writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) ();
+          (thy,NONE))
 
 fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
   let
isabelle