# HG changeset patch
# User wenzelm
# Date 1376034925 -7200
# Node ID 52d21bddcb8ac693d08c0d4dbff4847334d73c19
# Parent  facb4f6dc39173824935f37445acf7d071be5046
clarified toplevel_error: absorb and print interrupts;
tuned;

diff -r facb4f6dc391 -r 52d21bddcb8a src/Pure/PIDE/query_operation.ML
--- a/src/Pure/PIDE/query_operation.ML	Fri Aug 09 00:04:47 2013 +0200
+++ b/src/Pure/PIDE/query_operation.ML	Fri Aug 09 09:55:25 2013 +0200
@@ -22,19 +22,15 @@
             let
               fun result s = Output.result [(Markup.instanceN, instance)] s;
               fun status m = result (Markup.markup_only m);
-              fun error_msg exn =
-                if Exn.is_interrupt exn then reraise exn
-                else
-                  XML.Elem ((Markup.errorN, []), [XML.Text (ML_Compiler.exn_message exn)])
-                  |> YXML.string_of |> result;
+              fun toplevel_error exn =
+                result (Markup.markup (Markup.errorN, []) (ML_Compiler.exn_message exn));
 
               val _ = status Markup.running;
-              val outputs = f state args handle exn => (error_msg exn; []);
+              val outputs = f state args handle exn (*sic!*) => (toplevel_error exn; []);
               val _ = outputs |> Par_List.map (fn out =>
-                (case Exn.capture out () of
-                  Exn.Res s =>
-                    result (YXML.string_of (XML.Elem ((Markup.writelnN, []), [XML.Text s])))
-                | Exn.Exn exn => error_msg exn));
+                (case Exn.capture out () (*sic!*) of
+                  Exn.Res s => result (Markup.markup (Markup.writelnN, []) s)
+                | Exn.Exn exn => toplevel_error exn));
               val _ = status Markup.finished;
             in () end}
       | _ => NONE);