added message when Waldmeister isn't run
authorblanchet
Sun May 22 14:51:42 2011 +0200 (2011-05-22 ago)
changeset 42946ddff373cf3ad
parent 42945 cb28abfde010
child 42947 fcb6250bf6b4
added message when Waldmeister isn't run
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun May 22 14:51:42 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun May 22 14:51:42 2011 +0200
     1.3 @@ -168,8 +168,9 @@
     1.4  
     1.5  val auto_max_relevant_divisor = 2 (* FUDGE *)
     1.6  
     1.7 -fun run_sledgehammer (params as {debug, blocking, provers, relevance_thresholds,
     1.8 -                                 max_relevant, slicing, timeout, ...})
     1.9 +fun run_sledgehammer (params as {debug, verbose, blocking, provers,
    1.10 +                                 relevance_thresholds, max_relevant, slicing,
    1.11 +                                 timeout, ...})
    1.12          auto i (relevance_override as {only, ...}) minimize_command state =
    1.13    if null provers then
    1.14      error "No prover is set."
    1.15 @@ -244,8 +245,16 @@
    1.16                         ())
    1.17          end
    1.18        fun launch_atps label is_good_prop atps accum =
    1.19 -        if null atps orelse not (is_good_prop concl_t) then
    1.20 +        if null atps then
    1.21            accum
    1.22 +        else if not (is_good_prop concl_t) then
    1.23 +          (if verbose orelse length atps = length provers then
    1.24 +             "Goal outside the scope of " ^
    1.25 +             space_implode " " (serial_commas "and" (map quote atps)) ^ "."
    1.26 +             |> Output.urgent_message
    1.27 +           else
    1.28 +             ();
    1.29 +           accum)
    1.30          else
    1.31            launch_provers state
    1.32                (get_facts label is_good_prop atp_relevance_fudge o K atps)