1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 23 16:21:47 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 23 16:55:51 2010 +0200
     1.3 @@ -53,13 +53,13 @@
     1.4  val _ =
     1.5    ProofGeneralPgip.add_preference Preferences.category_proof
     1.6        (Preferences.int_pref timeout
     1.7 -          "Sledgehammer: Time limit"
     1.8 +          "Sledgehammer: Time Limit"
     1.9            "ATPs will be interrupted after this time (in seconds)")
    1.10  
    1.11  val _ =
    1.12    ProofGeneralPgip.add_preference Preferences.category_proof
    1.13        (Preferences.bool_pref full_types
    1.14 -          "Sledgehammer: Full types" "ATPs will use full type information")
    1.15 +          "Sledgehammer: Full Types" "ATPs will use full type information")
    1.16  
    1.17  type raw_param = string * string list
    1.18  
    1.19 @@ -196,6 +196,21 @@
    1.20  fun get_params thy = extract_params thy (default_raw_params thy)
    1.21  fun default_params thy = get_params thy o map (apsnd single)
    1.22  
    1.23 +(* Sledgehammer the given subgoal *)
    1.24 +
    1.25 +fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."
    1.26 +  | run (params as {atps, timeout, ...}) i relevance_override minimize_command
    1.27 +        proof_state =
    1.28 +    let
    1.29 +      val birth_time = Time.now ()
    1.30 +      val death_time = Time.+ (birth_time, timeout)
    1.31 +      val _ = kill_atps ()  (* race w.r.t. other invocations of Sledgehammer *)
    1.32 +      val _ = priority "Sledgehammering..."
    1.33 +      val _ = List.app (start_prover_thread params birth_time death_time i
    1.34 +                                            relevance_override minimize_command
    1.35 +                                            proof_state) atps
    1.36 +    in () end
    1.37 +
    1.38  fun minimize override_params old_style_args i fact_refs state =
    1.39    let
    1.40      val thy = Proof.theory_of state
    1.41 @@ -232,6 +247,9 @@
    1.42      priority (#2 (minimize_theorems params prover atp i state name_thms_pairs))
    1.43    end
    1.44  
    1.45 +val sledgehammerN = "sledgehammer"
    1.46 +val sledgehammer_paramsN = "sledgehammer_params"
    1.47 +
    1.48  val runN = "run"
    1.49  val minimizeN = "minimize"
    1.50  val messagesN = "messages"
    1.51 @@ -252,7 +270,7 @@
    1.52           | value => " = " ^ value)
    1.53  
    1.54  fun minimize_command override_params i atp_name facts =
    1.55 -  "sledgehammer minimize [atp = " ^ atp_name ^
    1.56 +  sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^
    1.57    (override_params |> filter is_raw_param_relevant_for_minimize
    1.58                     |> implode o map (prefix ", " o string_for_raw_param)) ^
    1.59    "] (" ^ space_implode " " facts ^ ")" ^
    1.60 @@ -265,8 +283,8 @@
    1.61    in
    1.62      if subcommand = runN then
    1.63        let val i = the_default 1 opt_i in
    1.64 -        sledgehammer (get_params thy override_params) i relevance_override
    1.65 -                     (minimize_command override_params i) state
    1.66 +        run (get_params thy override_params) i relevance_override
    1.67 +            (minimize_command override_params i) state
    1.68        end
    1.69      else if subcommand = minimizeN then
    1.70        minimize (map (apfst minimizize_raw_param_name) override_params) []
    1.71 @@ -355,11 +373,11 @@
    1.72          Toplevel.keep (minimize [] args 1 fact_refs o Toplevel.proof_of)))
    1.73  
    1.74  val _ =
    1.75 -  OuterSyntax.improper_command "sledgehammer"
    1.76 +  OuterSyntax.improper_command sledgehammerN
    1.77      "search for first-order proof using automatic theorem provers" K.diag
    1.78      parse_sledgehammer_command
    1.79  val _ =
    1.80 -  OuterSyntax.command "sledgehammer_params"
    1.81 +  OuterSyntax.command sledgehammer_paramsN
    1.82      "set and display the default parameters for Sledgehammer" K.thy_decl
    1.83      parse_sledgehammer_params_command
    1.84