src/Tools/quickcheck.ML
changeset 40491 87998864284e
parent 40466 2de5dd0cd3a2
child 40499 f99ec71de82d
     1.1 --- a/src/Tools/quickcheck.ML	Thu Oct 28 21:59:01 2010 +0200
     1.2 +++ b/src/Tools/quickcheck.ML	Thu Oct 28 22:04:00 2010 +0200
     1.3 @@ -139,9 +139,10 @@
     1.4  
     1.5  fun mk_testers_strict ctxt t =
     1.6    let
     1.7 -    val generators = ((map snd o fst o Data.get  o Context.Proof) ctxt)
     1.8 -    val testers = map (fn generator => Exn.capture (generator ctxt) t) generators;
     1.9 -  in if forall (is_none o Exn.get_result) testers
    1.10 +    val generators = ((map snd o fst o Data.get o Context.Proof) ctxt)
    1.11 +    val testers = map (fn generator => Exn.interruptible_capture (generator ctxt) t) generators;
    1.12 +  in
    1.13 +    if forall (is_none o Exn.get_result) testers
    1.14      then [(Exn.release o snd o split_last) testers]
    1.15      else map_filter Exn.get_result testers
    1.16    end;