clarified Query_Operation.register: avoid hard-wired parallel policy;
sledgehammer: more conventional parallel exception handling -- print just one interrupt;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 12 17:17:49 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 12 17:57:51 2013 +0200
@@ -496,42 +496,43 @@
 val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
 
 val _ =
-  Query_Operation.register_parallel sledgehammerN
-    (fn st => fn [provers_arg, timeout_arg, subgoal_arg, isar_proofs_arg] =>
-      (case try Toplevel.proof_of st of
-        SOME state =>
-          let
-            val ctxt = Proof.context_of state
+  Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
+    (case try Toplevel.proof_of st of
+      SOME state =>
+        let
+          val [provers_arg, timeout_arg, subgoal_arg, isar_proofs_arg] = args;
+          val ctxt = Proof.context_of state
 
-            val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt []
-            val override_params =
-              ([("timeout", [timeout_arg]),
-                ("blocking", ["true"])] @
-              (if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg
-               then [("isar_proofs", [isar_proofs_arg])] else []) @
-              (if debug then [("debug", ["false"])] else []) @
-              (if verbose then [("verbose", ["false"])] else []) @
-              (if overlord then [("overlord", ["false"])] else []))
-              |> map (normalize_raw_param ctxt)
+          val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt []
+          val override_params =
+            ([("timeout", [timeout_arg]),
+              ("blocking", ["true"])] @
+            (if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg
+             then [("isar_proofs", [isar_proofs_arg])] else []) @
+            (if debug then [("debug", ["false"])] else []) @
+            (if verbose then [("verbose", ["false"])] else []) @
+            (if overlord then [("overlord", ["false"])] else []))
+            |> map (normalize_raw_param ctxt)
 
-            val i = the_default 1 (Int.fromString subgoal_arg)
+          val i = the_default 1 (Int.fromString subgoal_arg)
 
-            val {provers, ...} =
-              get_params Normal ctxt
-                (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)])
+          val {provers, ...} =
+            get_params Normal ctxt
+              (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)])
 
-            fun run prover =
-              let
-                val prover_params = ("provers", [prover]) :: override_params
-                val sledgehammer_params = get_params Normal ctxt prover_params
-                val minimize = minimize_command prover_params i
-                val (_, (_, state')) =
-                  state
-                  |> Proof.map_context (Config.put sledgehammer_result_request true)
-                  |> run_sledgehammer sledgehammer_params Try i no_fact_override minimize
-              in Config.get (Proof.context_of state') sledgehammer_result end
+          fun run prover =
+            let
+              val prover_params = ("provers", [prover]) :: override_params
+              val sledgehammer_params = get_params Normal ctxt prover_params
+              val minimize = minimize_command prover_params i
+              val (_, (_, state')) =
+                state
+                |> Proof.map_context (Config.put sledgehammer_result_request true)
+                |> run_sledgehammer sledgehammer_params Try i no_fact_override minimize
+            in output_result (Config.get (Proof.context_of state') sledgehammer_result) end
 
-          in map (fn prover => fn () => run prover) provers end
-      | NONE => error "Unknown proof context"));
+          val _ = Par_Exn.release_all (Par_List.map (Exn.interruptible_capture run) provers);
+        in () end
+    | NONE => error "Unknown proof context"));
 
 end;

--- 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;
 

--- a/src/Pure/Tools/find_theorems.ML	Mon Aug 12 17:17:49 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Mon Aug 12 17:57:51 2013 +0200
@@ -575,17 +575,17 @@
 (** PIDE query operation **)
 
 val _ =
-  Query_Operation.register "find_theorems"
-    (fn st => fn [limit_arg, allow_dups_arg, context_arg, query_arg] =>
-      if can Toplevel.context_of st then
-        let
-          val state =
-            if context_arg = "" then proof_state st
-            else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
-          val opt_limit = Int.fromString limit_arg;
-          val rem_dups = allow_dups_arg = "false";
-          val criteria = read_query Position.none query_arg;
-        in Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria) end
-      else error "Unknown context");
+  Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
+    if can Toplevel.context_of st then
+      let
+        val [limit_arg, allow_dups_arg, context_arg, query_arg] = args;
+        val state =
+          if context_arg = "" then proof_state st
+          else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
+        val opt_limit = Int.fromString limit_arg;
+        val rem_dups = allow_dups_arg = "false";
+        val criteria = read_query Position.none query_arg;
+      in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
+    else error "Unknown context");
 
 end;