equal
deleted
inserted
replaced
137 (map snd o fst o Data.get o Context.Proof) ctxt |
137 (map snd o fst o Data.get o Context.Proof) ctxt |
138 |> map_filter (fn generator => try (generator ctxt) t); |
138 |> map_filter (fn generator => try (generator ctxt) t); |
139 |
139 |
140 fun mk_testers_strict ctxt t = |
140 fun mk_testers_strict ctxt t = |
141 let |
141 let |
142 val generators = ((map snd o fst o Data.get o Context.Proof) ctxt) |
142 val generators = ((map snd o fst o Data.get o Context.Proof) ctxt) |
143 val testers = map (fn generator => Exn.capture (generator ctxt) t) generators; |
143 val testers = map (fn generator => Exn.interruptible_capture (generator ctxt) t) generators; |
144 in if forall (is_none o Exn.get_result) testers |
144 in |
|
145 if forall (is_none o Exn.get_result) testers |
145 then [(Exn.release o snd o split_last) testers] |
146 then [(Exn.release o snd o split_last) testers] |
146 else map_filter Exn.get_result testers |
147 else map_filter Exn.get_result testers |
147 end; |
148 end; |
148 |
149 |
149 |
150 |