sledgehammer panel operation re-uses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;
authorwenzelm
Fri May 08 15:32:27 2015 +0200 (2015-05-08)
changeset 60277bcd9a70342be
parent 60276 3bb094031275
child 60278 2a9bc6447779
sledgehammer panel operation re-uses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri May 08 15:07:27 2015 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri May 08 15:32:27 2015 +0200
     1.3 @@ -296,7 +296,7 @@
     1.4  
     1.5  val default_learn_prover_timeout = 2.0
     1.6  
     1.7 -fun hammer_away override_params subcommand opt_i fact_override state0 =
     1.8 +fun hammer_away override_params output_result subcommand opt_i fact_override state0 =
     1.9    let
    1.10      (* We generally want chained facts to be picked up by the relevance filter, because it can then
    1.11         give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs,
    1.12 @@ -324,8 +324,9 @@
    1.13    in
    1.14      if subcommand = runN then
    1.15        let val i = the_default 1 opt_i in
    1.16 -        ignore (run_sledgehammer (get_params Normal thy override_params) Normal NONE i fact_override
    1.17 -          state)
    1.18 +        ignore
    1.19 +          (run_sledgehammer
    1.20 +            (get_params Normal thy override_params) Normal output_result i fact_override state)
    1.21        end
    1.22      else if subcommand = messagesN then
    1.23        messages opt_i
    1.24 @@ -378,10 +379,11 @@
    1.25  val _ =
    1.26    Outer_Syntax.command @{command_keyword sledgehammer}
    1.27      "search for first-order proof using automatic theorem provers"
    1.28 -    ((Scan.optional Parse.name runN -- parse_params
    1.29 -      -- parse_fact_override -- Scan.option Parse.nat) >>
    1.30 +    (Scan.optional Parse.name runN -- parse_params
    1.31 +      -- parse_fact_override -- Scan.option Parse.nat >>
    1.32        (fn (((subcommand, params), fact_override), opt_i) =>
    1.33 -        Toplevel.keep_proof (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of)))
    1.34 +        Toplevel.keep_proof
    1.35 +          (hammer_away params NONE subcommand opt_i fact_override o Toplevel.proof_of)))
    1.36  val _ =
    1.37    Outer_Syntax.command @{command_keyword sledgehammer_params}
    1.38      "set and display the default parameters for Sledgehammer"
    1.39 @@ -407,24 +409,17 @@
    1.40    Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
    1.41      (case try Toplevel.proof_of st of
    1.42        SOME state =>
    1.43 -      let
    1.44 -        val thy = Proof.theory_of state
    1.45 -        val ctxt = Proof.context_of state
    1.46 -        val [provers_arg, isar_proofs_arg, try0_arg] = args
    1.47 -
    1.48 -        val override_params =
    1.49 -          ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
    1.50 -            [("isar_proofs", [isar_proofs_arg]),
    1.51 -             ("try0", [try0_arg]),
    1.52 -             ("blocking", ["true"]),
    1.53 -             ("debug", ["false"]),
    1.54 -             ("verbose", ["false"]),
    1.55 -             ("overlord", ["false"])])
    1.56 -          |> map (normalize_raw_param ctxt)
    1.57 -      in
    1.58 -        ignore (run_sledgehammer (get_params Normal thy override_params) Normal
    1.59 -          (SOME output_result) 1 no_fact_override state)
    1.60 -      end
    1.61 +        let
    1.62 +          val [provers_arg, isar_proofs_arg, try0_arg] = args
    1.63 +          val override_params =
    1.64 +            ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
    1.65 +              [("isar_proofs", [isar_proofs_arg]),
    1.66 +               ("try0", [try0_arg]),
    1.67 +               ("blocking", ["true"]),
    1.68 +               ("debug", ["false"]),
    1.69 +               ("verbose", ["false"]),
    1.70 +               ("overlord", ["false"])]);
    1.71 +        in hammer_away override_params (SOME output_result) runN NONE no_fact_override state end
    1.72      | NONE => error "Unknown proof context"))
    1.73  
    1.74  end;