1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:07 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:07 2011 +0200
     1.3 @@ -31,16 +31,16 @@
     1.4  
     1.5  fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
     1.6                         n goal =
     1.7 -  quote name ^
     1.8 -  (if verbose then
     1.9 -     " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
    1.10 -   else
    1.11 -     "") ^
    1.12 -  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
    1.13 -  (if blocking then
    1.14 -     "."
    1.15 -   else
    1.16 -     ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
    1.17 +  (name,
    1.18 +   (if verbose then
    1.19 +      " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
    1.20 +    else
    1.21 +      "") ^
    1.22 +   " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
    1.23 +   (if blocking then
    1.24 +      "."
    1.25 +    else
    1.26 +      ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
    1.27  
    1.28  val auto_minimize_min_facts =
    1.29    Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
    1.30 @@ -86,6 +86,11 @@
    1.31               | NONE => result
    1.32             end)
    1.33  
    1.34 +val someN = "some"
    1.35 +val noneN = "none"
    1.36 +val timeoutN = "timeout"
    1.37 +val unknownN = "unknown"
    1.38 +
    1.39  fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
    1.40                                expect, ...})
    1.41          auto minimize_command only
    1.42 @@ -109,7 +114,9 @@
    1.43        problem
    1.44        |> get_minimizing_prover ctxt auto name params (minimize_command name)
    1.45        |> (fn {outcome, message, ...} =>
    1.46 -             (if is_some outcome then "none" else "some" (* sic *), message))
    1.47 +             (if outcome = SOME ATP_Proof.TimedOut then timeoutN
    1.48 +              else if is_some outcome then noneN
    1.49 +              else someN, message))
    1.50      fun go () =
    1.51        let
    1.52          val (outcome_code, message) =
    1.53 @@ -117,13 +124,13 @@
    1.54              really_go ()
    1.55            else
    1.56              (really_go ()
    1.57 -             handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
    1.58 +             handle ERROR message => (unknownN, "Error: " ^ message ^ "\n")
    1.59                    | exn =>
    1.60                      if Exn.is_interrupt exn then
    1.61                        reraise exn
    1.62                      else
    1.63 -                      ("unknown", "Internal error:\n" ^
    1.64 -                                  ML_Compiler.exn_message exn ^ "\n"))
    1.65 +                      (unknownN, "Internal error:\n" ^
    1.66 +                                ML_Compiler.exn_message exn ^ "\n"))
    1.67          val _ =
    1.68            (* The "expect" argument is deliberately ignored if the prover is
    1.69               missing so that the "Metis_Examples" can be processed on any
    1.70 @@ -135,22 +142,27 @@
    1.71              error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
    1.72            else
    1.73              warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
    1.74 -      in (outcome_code = "some", message) end
    1.75 +      in (outcome_code, message) end
    1.76    in
    1.77      if auto then
    1.78 -      let val (success, message) = TimeLimit.timeLimit timeout go () in
    1.79 +      let
    1.80 +        val (outcome_code, message) = TimeLimit.timeLimit timeout go ()
    1.81 +        val success = (outcome_code = someN)
    1.82 +      in
    1.83          (success, state |> success ? Proof.goal_message (fn () =>
    1.84               Pretty.chunks [Pretty.str "",
    1.85                              Pretty.mark Markup.hilite (Pretty.str message)]))
    1.86        end
    1.87      else if blocking then
    1.88 -      let val (success, message) = TimeLimit.timeLimit hard_timeout go () in
    1.89 -        List.app Output.urgent_message
    1.90 -                 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
    1.91 -        (success, state)
    1.92 +      let val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () in
    1.93 +        Async_Manager.implode_desc desc ^ "\n" ^ message
    1.94 +        |> Async_Manager.break_into_chunks
    1.95 +        |> List.app Output.urgent_message;
    1.96 +        (outcome_code = someN, state)
    1.97        end
    1.98      else
    1.99 -      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
   1.100 +      (Async_Manager.launch das_tool birth_time death_time desc
   1.101 +                            (apfst (curry (op <>) timeoutN) o go);
   1.102         (false, state))
   1.103    end
   1.104