# HG changeset patch
# User blanchet
# Date 1306767638 -7200
# Node ID 95b845a0edce749be2c6f8ac680c3d29c524eea1
# Parent  5f8bac7a2945781508c5d3f96abecc533678406c
make all messages urgent in verbose mode

diff -r 5f8bac7a2945 -r 95b845a0edce src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 30 17:00:38 2011 +0200
@@ -134,8 +134,8 @@
              | NONE => result
            end)
 
-fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
-                              expect, ...})
+fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,
+                              timeout, expect, ...})
         mode minimize_command only
         {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
   let
@@ -212,7 +212,8 @@
     else
       (Async_Manager.launch das_tool birth_time death_time (desc ())
                             ((fn (outcome_code, message) =>
-                                 (outcome_code = someN, message ())) o go);
+                                 (verbose orelse outcome_code = someN,
+                                  message ())) o go);
        (unknownN, state))
   end