src/Pure/PIDE/query_operation.ML

--- a/src/Pure/PIDE/query_operation.ML	Mon Aug 12 17:17:49 2013 +0200
+++ b/src/Pure/PIDE/query_operation.ML	Mon Aug 12 17:57:51 2013 +0200
@@ -7,14 +7,14 @@
 
 signature QUERY_OPERATION =
 sig
-  val register_parallel: string -> (Toplevel.state -> string list -> (unit -> string) list) -> unit
-  val register: string -> (Toplevel.state -> string list -> string) -> unit
+  val register: string ->
+    ({state: Toplevel.state, args: string list, output_result: string -> unit} -> unit) -> unit
 end;
 
 structure Query_Operation: QUERY_OPERATION =
 struct
 
-fun register_parallel name f =
+fun register name f =
   Command.print_function name
     (fn {args = instance :: args, ...} =>
         SOME {delay = NONE, pri = 0, persistent = false, strict = false,
@@ -22,23 +22,19 @@
             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.writelnN, []) s);
               fun toplevel_error exn =
                 result (Markup.markup (Markup.errorN, []) (ML_Compiler.exn_message exn));
 
               val _ = status Markup.running;
-              val outputs =
-                Multithreading.interruptible (fn () => f state args) ()
-                  handle exn (*sic!*) => (toplevel_error exn; []);
-              val _ = outputs |> Par_List.map (fn out =>
-                (case Exn.capture (restore_attributes out) () (*sic!*) of
-                  Exn.Res s => result (Markup.markup (Markup.writelnN, []) s)
-                | Exn.Exn exn => toplevel_error exn));
+              fun run () = f {state = state, args = args, output_result = output_result};
+              val _ =
+                (case Exn.capture (*sic!*) (restore_attributes run) () of
+                  Exn.Res () => ()
+                | Exn.Exn exn => toplevel_error exn);
               val _ = status Markup.finished;
             in () end)}
       | _ => NONE);
 
-fun register name f =
-  register_parallel name (fn st => fn args => [fn () => f st args]);
-
 end;