1.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 12 14:54:17 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 12 15:37:48 2013 +0200
     1.3 @@ -135,7 +135,9 @@
     1.4      (fn () =>
     1.5        Outer_Syntax.side_comments span |> maps (fn cmt =>
     1.6          (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
     1.7 -          handle exn => ML_Compiler.exn_messages_ids exn)) ();
     1.8 +          handle exn =>
     1.9 +            if Exn.is_interrupt exn then reraise exn
    1.10 +            else ML_Compiler.exn_messages_ids exn)) ();
    1.11  
    1.12  fun proof_status tr st =
    1.13    (case try Toplevel.proof_of st of
    1.14 @@ -201,8 +203,10 @@
    1.15  val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
    1.16  
    1.17  fun print_error tr e =
    1.18 -  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn =>
    1.19 -    List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
    1.20 +  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e ()
    1.21 +    handle exn =>
    1.22 +      if Exn.is_interrupt exn then reraise exn
    1.23 +      else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
    1.24  
    1.25  fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.26