src/Pure/codegen.ML
changeset 25400 e05b9fa43885
parent 25376 87824cc5ff90
child 25892 3ff9d646a66a
     1.1 --- a/src/Pure/codegen.ML	Sun Nov 11 16:50:29 2007 +0100
     1.2 +++ b/src/Pure/codegen.ML	Sun Nov 11 16:50:30 2007 +0100
     1.3 @@ -992,19 +992,17 @@
     1.4      val ctxt = Proof.context_of state;
     1.5      val assms = map term_of (Assumption.assms_of ctxt);
     1.6      val params = get_test_params (Proof.theory_of state);
     1.7 -    fun report msg = (Output.priority ("Auto quickcheck: " ^ msg); state);
     1.8      fun test () =
     1.9        let
    1.10 -        val _ = Output.priority "Auto quickcheck ...";
    1.11          val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
    1.12            (try (test_goal true (params, []) 1 assms)) state;
    1.13        in
    1.14          case res of
    1.15 -          NONE => report "failed."
    1.16 -        | SOME NONE => report "no counterexamples found."
    1.17 +          NONE => state
    1.18 +        | SOME NONE => state
    1.19          | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
    1.20              Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
    1.21 -      end handle TimeLimit.TimeOut => report "timeout.";
    1.22 +      end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
    1.23    in
    1.24      if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
    1.25      then test ()