# HG changeset patch # User wenzelm # Date 1376323071 -7200 # Node ID 8e78bd316a535e0a8f4f703242694d79e9c04325 # Parent c7afd884dfb2599fc34f33278ff1e8d5d66457e0 clarified Query_Operation.register: avoid hard-wired parallel policy; sledgehammer: more conventional parallel exception handling -- print just one interrupt; diff -r c7afd884dfb2 -r 8e78bd316a53 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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; diff -r c7afd884dfb2 -r 8e78bd316a53 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; diff -r c7afd884dfb2 -r 8e78bd316a53 src/Pure/Tools/find_theorems.ML --- 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;