equal
deleted
inserted
replaced
282 else ()) |
282 else ()) |
283 |
283 |
284 val succs = collect_successors steps' succ_lbls |
284 val succs = collect_successors steps' succ_lbls |
285 val succs' = map (try_merge cand #> the) succs |
285 val succs' = map (try_merge cand #> the) succs |
286 |
286 |
|
287 (* TODO: should be lazy: stop preplaying as soon as one step |
|
288 fails/times out *) |
287 val preplay_times = |
289 val preplay_times = |
288 map (uncurry preplay_quietly) (timeouts ~~ succs') |
290 map (uncurry preplay_quietly) (timeouts ~~ succs') |
289 |
291 |
290 (* ensure none of the modified successors timed out *) |
292 (* ensure none of the modified successors timed out *) |
291 val false = List.exists fst preplay_times |
293 val false = List.exists fst preplay_times |