diff -r 05d28dc76e5c -r dfccf6c06201 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 () => ()