--- a/src/Pure/PIDE/query_operation.ML Tue Aug 06 17:30:09 2013 +0200
+++ b/src/Pure/PIDE/query_operation.ML Tue Aug 06 21:08:04 2013 +0200
@@ -19,11 +19,17 @@
SOME {delay = NONE, pri = 0, persistent = false,
print_fn = fn _ => fn state =>
let
+ fun result s = Output.result [(Markup.instanceN, instance)] s;
+ fun status m = result (Markup.markup_only m);
+
+ val _ = status Markup.running;
val msg = XML.Elem ((Markup.writelnN, []), [XML.Text (f state args)])
handle exn =>
if Exn.is_interrupt exn then reraise exn
else XML.Elem ((Markup.errorN, []), [XML.Text (ML_Compiler.exn_message exn)]);
- in Output.result [(Markup.instanceN, instance)] (YXML.string_of msg) end}
+ val _ = result (YXML.string_of msg);
+ val _ = status Markup.finished;
+ in () end}
| _ => NONE);
end;