# HG changeset patch
# User bulwahn
# Date 1297186776 -3600
# Node ID bd7ee90267f27cd4700319e3ccc9d5febaf70641
# Parent  ae1a46cdb9cb24be4bf290942225181917216a89
changing auto-quickcheck to be considered a non-interactive invocation of quickcheck

diff -r ae1a46cdb9cb -r bd7ee90267f2 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Tue Feb 08 17:44:53 2011 +0100
+++ b/src/Tools/quickcheck.ML	Tue Feb 08 18:39:36 2011 +0100
@@ -299,7 +299,7 @@
       collect_results (test_term lthy is_interactive) [] (maps (map snd) correct_inst_goals)
   end;
 
-fun test_goal insts i state =
+fun test_goal is_interactive insts i state =
   let
     val lthy = Proof.context_of state;
     val thy = Proof.theory_of state;
@@ -320,7 +320,7 @@
       | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
         (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
   in
-    test_goal_terms lthy true insts check_goals
+    test_goal_terms lthy is_interactive insts check_goals
   end
 
 (* pretty printing *)
@@ -365,7 +365,7 @@
     val res =
       state
       |> Proof.map_context (Config.put report false #> Config.put quiet true)
-      |> try (test_goal [] 1);
+      |> try (test_goal false [] 1);
   in
     case res of
       NONE => (false, state)
@@ -436,7 +436,7 @@
 fun gen_quickcheck args i state =
   state
   |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ([], ctxt))
-  |> (fn (insts, state') => test_goal insts i state'
+  |> (fn (insts, state') => test_goal true insts i state'
   |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
                error ("quickcheck expected to find no counterexample but found one") else ()
            | (NONE, _) => if expect (Proof.context_of state') = Counterexample then