refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
authorwenzelm
Thu Sep 09 18:21:06 2010 +0200 (2010-09-09)
changeset 392387189a138dd6c
parent 39237 be1acdcd55dc
child 39239 47273e5b1441
refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
src/Pure/Isar/runtime.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/Isar/runtime.ML	Thu Sep 09 18:18:34 2010 +0200
     1.2 +++ b/src/Pure/Isar/runtime.ML	Thu Sep 09 18:21:06 2010 +0200
     1.3 @@ -110,9 +110,14 @@
     1.4    |> debugging
     1.5    |> Future.interruptible_task;
     1.6  
     1.7 -fun toplevel_error output_exn f x =
     1.8 -  let val ctxt = Option.map Context.proof_of (Context.thread_data ())
     1.9 -  in f x handle exn => (output_exn (exn_context ctxt exn); raise TOPLEVEL_ERROR) end;
    1.10 +fun toplevel_error output_exn f x = f x
    1.11 +  handle exn =>
    1.12 +    if Exn.is_interrupt exn then reraise exn
    1.13 +    else
    1.14 +      let
    1.15 +        val ctxt = Option.map Context.proof_of (Context.thread_data ());
    1.16 +        val _ = output_exn (exn_context ctxt exn);
    1.17 +      in raise TOPLEVEL_ERROR end;
    1.18  
    1.19  end;
    1.20  
     2.1 --- a/src/Pure/PIDE/document.ML	Thu Sep 09 18:18:34 2010 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Sep 09 18:21:06 2010 +0200
     2.3 @@ -238,7 +238,10 @@
     2.4                if int then () else async_state tr st'));
     2.5        in result end
     2.6    | Exn.Exn exn =>
     2.7 -     (Toplevel.error_msg tr (ML_Compiler.exn_message exn); Toplevel.status tr Markup.failed; NONE))
     2.8 +      if Exn.is_interrupt exn then reraise exn
     2.9 +      else
    2.10 +       (Toplevel.error_msg tr (ML_Compiler.exn_message exn);
    2.11 +        Toplevel.status tr Markup.failed; NONE));
    2.12  
    2.13  end;
    2.14