src/Pure/PIDE/query_operation.ML

--- a/src/Pure/PIDE/query_operation.ML	Mon Sep 21 21:46:14 2015 +0200
+++ b/src/Pure/PIDE/query_operation.ML	Mon Sep 21 23:22:11 2015 +0200
@@ -8,7 +8,8 @@
 signature QUERY_OPERATION =
 sig
   val register: {name: string, pri: int} ->
-    ({state: Toplevel.state, args: string list, output_result: string -> unit} -> unit) -> unit
+    ({state: Toplevel.state, args: string list,
+      output_result: string -> unit, writeln_result: string -> unit} -> unit) -> unit
 end;
 
 structure Query_Operation: QUERY_OPERATION =
@@ -20,13 +21,16 @@
       SOME {delay = NONE, pri = pri, persistent = false, strict = false,
         print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
           let
-            fun result s = Output.result [(Markup.instanceN, instance)] [s];
-            fun status m = result (Markup.markup_only m);
-            fun output_result s = result (Markup.markup Markup.writeln s);
-            fun toplevel_error exn = result (Markup.markup Markup.error (Runtime.exn_message exn));
+            fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
+            fun status m = output_result (Markup.markup_only m);
+            fun writeln_result s = output_result (Markup.markup Markup.writeln s);
+            fun toplevel_error exn =
+              output_result (Markup.markup Markup.error (Runtime.exn_message exn));
 
             val _ = status Markup.running;
-            fun run () = f {state = state, args = args, output_result = output_result};
+            fun run () =
+              f {state = state, args = args, output_result = output_result,
+                  writeln_result = writeln_result};
             val _ =
               (case Exn.capture (*sic!*) (restore_attributes run) () of
                 Exn.Res () => ()