# HG changeset patch
# User wenzelm
# Date 1373636268 -7200
# Node ID 70d5f2f7d27f6f8dc30cac9b8e830bdf01d9d244
# Parent  2077168aa8f7b53eeb1684d139a816e5769a6775
reraise interrupts outside command regular transactions -- relevant for memo_stable;

diff -r 2077168aa8f7 -r 70d5f2f7d27f src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Jul 12 14:54:17 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Jul 12 15:37:48 2013 +0200
@@ -135,7 +135,9 @@
     (fn () =>
       Outer_Syntax.side_comments span |> maps (fn cmt =>
         (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
-          handle exn => ML_Compiler.exn_messages_ids exn)) ();
+          handle exn =>
+            if Exn.is_interrupt exn then reraise exn
+            else ML_Compiler.exn_messages_ids exn)) ();
 
 fun proof_status tr st =
   (case try Toplevel.proof_of st of
@@ -201,8 +203,10 @@
 val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
 
 fun print_error tr e =
-  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn =>
-    List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
+  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e ()
+    handle exn =>
+      if Exn.is_interrupt exn then reraise exn
+      else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
 
 fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';