1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Jul 20 08:16:39 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Jul 20 08:16:41 2011 +0200
     1.3 @@ -285,9 +285,9 @@
     1.4              end 
     1.5        in with_size 0 end
     1.6    in
     1.7 -    Quickcheck.limit timeout (limit_time, is_interactive) 
     1.8 -      (fn () => with_tmp_dir tmp_prefix run)
     1.9 -      (fn () => (message (excipit ()); (NONE, !current_result))) ()
    1.10 +    (*Quickcheck.limit timeout (limit_time, is_interactive) 
    1.11 +      (fn () =>*) with_tmp_dir tmp_prefix run
    1.12 +      (*(fn () => (message (excipit ()); (NONE, !current_result))) ()*)
    1.13    end;
    1.14  
    1.15  fun dynamic_value_strict opts cookie thy postproc t =

     2.1 --- a/src/Tools/quickcheck.ML	Wed Jul 20 08:16:39 2011 +0200
     2.2 +++ b/src/Tools/quickcheck.ML	Wed Jul 20 08:16:41 2011 +0200
     2.3 @@ -319,7 +319,7 @@
     2.4            case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q
     2.5          end;
     2.6    in
     2.7 -    limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>
     2.8 +    (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)(
     2.9        let
    2.10          val (test_fun, comp_time) = cpu_time "quickcheck compilation"
    2.11            (fn () => compile ctxt [(t, eval_terms)]);
    2.12 @@ -329,7 +329,7 @@
    2.13          val _ = add_response names eval_terms response current_result
    2.14          val _ = add_timing exec_time current_result
    2.15        in !current_result end)
    2.16 -    (fn () => (message (excipit ()); !current_result)) ()
    2.17 +(*    (fn () => (message (excipit ()); !current_result)) ()*)
    2.18    end;
    2.19  
    2.20  fun validate_terms ctxt ts =
    2.21 @@ -399,7 +399,7 @@
    2.22          map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size))
    2.23          |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
    2.24    in
    2.25 -    limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>
    2.26 +    (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)(
    2.27        let
    2.28          val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts)
    2.29          val _ = add_timing comp_time current_result     
    2.30 @@ -407,7 +407,7 @@
    2.31            SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
    2.32          | NONE => ()
    2.33        in !current_result end)
    2.34 -      (fn () => (message "Quickcheck ran out of time"; !current_result)) ()
    2.35 +      (*(fn () => (message "Quickcheck ran out of time"; !current_result)) ()*)
    2.36    end
    2.37  
    2.38  fun get_finite_types ctxt =
    2.39 @@ -490,14 +490,18 @@
    2.40        collect_results (test_term compile ctxt (limit_time, is_interactive))
    2.41          (maps (map snd) correct_inst_goals) []
    2.42    end;
    2.43 +
    2.44 +fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s
    2.45    
    2.46  fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
    2.47    case active_testers ctxt of
    2.48      [] => error "No active testers for quickcheck"
    2.49 -  | testers => testers |> Par_List.get_some (fn tester =>
    2.50 +  | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
    2.51 +      (fn () => Par_List.get_some (fn tester =>
    2.52        tester ctxt (limit_time, is_interactive) insts goals |>
    2.53 -      (fn result => if exists found_counterexample result then SOME result else NONE))
    2.54 -
    2.55 +      (fn result => if exists found_counterexample result then SOME result else NONE)) testers)
    2.56 +      (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ();
    2.57 +      
    2.58  fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
    2.59    let
    2.60      val lthy = Proof.context_of state;