making the default behaviour of quickcheck a little bit less verbose;
adapting quickcheck examples

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Dec 05 12:36:21 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Dec 05 12:36:22 2011 +0100
@@ -222,10 +222,11 @@
   let val ({elapsed, ...}, result) = Timing.timing e ()
   in (result, (description, Time.toMilliseconds elapsed)) end
   
-fun value (contains_existentials, ((genuine_only, quiet), size)) ctxt cookie (code, value_name) =
+fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code, value_name) =
   let
     val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
     fun message s = if quiet then () else Output.urgent_message s
+    fun verbose_message s = if not quiet andalso verbose then Output.urgent_message s else ()
     val current_size = Unsynchronized.ref 0
     val current_result = Unsynchronized.ref Quickcheck.empty_result 
     fun excipit () =
@@ -265,7 +266,7 @@
             (NONE, !current_result)
           else
             let
-              val _ = message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
+              val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
               val _ = current_size := k
               val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
                 (fn () => Isabelle_System.bash_output
@@ -292,8 +293,8 @@
                     let
                       val cex = Option.map (rpair []) (counterexample_of counterexample)
                     in
-                      (Output.urgent_message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
-                      Output.urgent_message "Quickcheck continues to find a genuine counterexample...";
+                      (message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+                      message "Quickcheck continues to find a genuine counterexample...";
                       with_size true (k + 1))
                     end
                end
@@ -431,7 +432,8 @@
   let
     fun dest_result (Quickcheck.Result r) = r 
     val opts =
-      ((Config.get ctxt Quickcheck.genuine_only, Config.get ctxt Quickcheck.quiet),
+      ((Config.get ctxt Quickcheck.genuine_only,
+       (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.verbose)),
         Config.get ctxt Quickcheck.size)
     val thy = Proof_Context.theory_of ctxt
     val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
@@ -480,6 +482,7 @@
 fun test_goals ctxt _ insts goals =
   if (not (getenv "ISABELLE_GHC" = "")) then
     let
+      val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-narrowing...")
       val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
     in
       Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) []

--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Dec 05 12:36:21 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Dec 05 12:36:22 2011 +0100
@@ -85,7 +85,7 @@
         NONE
       else
         let
-          val _ = Quickcheck.message ctxt
+          val _ = Quickcheck.verbose_message ctxt
             ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
           val _ = current_size := k
           val ((result, report), timing) =
@@ -102,8 +102,8 @@
               val (eval_terms', _) = chop (length ts2) eval_terms
               val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
             in
-              (Output.urgent_message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
-              Output.urgent_message "Quickcheck continues to find a genuine counterexample...";
+              (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+              Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
               with_size test_fun true k)
             end
         end;
@@ -171,7 +171,7 @@
       (* FIXME: why decrement size by one? *)
       let
         val _ =
-          Quickcheck.message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
+          Quickcheck.verbose_message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
             (if size = 0 then "" else "data size: " ^ string_of_int (size - 1) ^ " and ") ^
             "cardinality: " ^ string_of_int card)          
         val (ts, timing) =
@@ -198,6 +198,7 @@
         !current_result)
     | SOME test_fun =>
       let
+        val _ = Quickcheck.message ctxt ("Testing conjecture with with Quickcheck-" ^ name ^ "...");
         fun test genuine_only enum = case get_first (test_card_size test_fun genuine_only) enum of
           SOME ((card, _), (true, ts)) =>
             Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (true, ts)) current_result
@@ -207,8 +208,8 @@
               val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1))
               val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
             in
-              (Output.urgent_message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
-              Output.urgent_message "Quickcheck continues to find a genuine counterexample...";
+              (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+              Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
               test true (snd (take_prefix (fn x => not (x = (card, size))) enum)))
             end
         | NONE => ()

--- a/src/HOL/ex/Quickcheck_Examples.thy	Mon Dec 05 12:36:21 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Mon Dec 05 12:36:22 2011 +0100
@@ -413,22 +413,20 @@
   "xs = [] ==> hd xs \<noteq> x"
 quickcheck[exhaustive, expect = no_counterexample]
 quickcheck[random, report = false, expect = no_counterexample]
-quickcheck[random, report = true, expect = counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
 oops
 
 lemma
   "xs = [] ==> hd xs = x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
-quickcheck[random, potential = false, report = false, expect = no_counterexample]
-quickcheck[random, potential = true, report = false, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
 oops
 
 lemma "xs = [] ==> hd xs = x ==> x = y"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
-quickcheck[random, potential = false, report = false, expect = no_counterexample]
-quickcheck[random, potential = true, report = false, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
 oops
 
 text {* with the simple testing scheme *}
@@ -438,19 +436,16 @@
 
 lemma
   "xs = [] ==> hd xs \<noteq> x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
 oops
 
 lemma
   "xs = [] ==> hd xs = x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
 oops
 
 lemma "xs = [] ==> hd xs = x ==> x = y"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
 oops
 
 declare [[quickcheck_full_support = true]]

--- a/src/Tools/quickcheck.ML	Mon Dec 05 12:36:21 2011 +0100
+++ b/src/Tools/quickcheck.ML	Mon Dec 05 12:36:22 2011 +0100
@@ -63,6 +63,7 @@
       -> Context.generic -> Context.generic
   (* basic operations *)
   val message : Proof.context -> string -> unit
+  val verbose_message : Proof.context -> string -> unit
   val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a
   val pretty_counterex : Proof.context -> bool ->
     ((bool * (string * term) list) * (term * term) list) option -> Pretty.T
@@ -292,11 +293,15 @@
     f ()
 
 fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s
-  
+
+fun verbose_message ctxt s = if not (Config.get ctxt quiet) andalso Config.get ctxt verbose
+  then Output.urgent_message s else ()
+
 fun test_terms ctxt (limit_time, is_interactive) insts goals =
   case active_testers ctxt of
     [] => error "No active testers for quickcheck"
-  | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
+  | testers =>
+    limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
       (fn () => Par_List.get_some (fn tester =>
       tester ctxt (length testers > 1) insts goals |>
       (fn result => if exists found_counterexample result then SOME result else NONE)) testers)
@@ -306,6 +311,7 @@
   let
     val lthy = Proof.context_of state;
     val thy = Proof.theory_of state;
+    val _ = message lthy "Quickchecking..."
     fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
       | strip t = t;
     val {goal = st, ...} = Proof.raw_goal state;