equal
deleted
inserted
replaced
31 fun try0_step _ _ _ (step as Let _) = step |
31 fun try0_step _ _ _ (step as Let _) = step |
32 | try0_step ctxt preplay_timeout preplay_data |
32 | try0_step ctxt preplay_timeout preplay_data |
33 (step as Prove (_, _, l, _, _, (_, meths as meth :: _))) = |
33 (step as Prove (_, _, l, _, _, (_, meths as meth :: _))) = |
34 let |
34 let |
35 val timeout = |
35 val timeout = |
36 (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of |
36 (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
37 Played time => Time.+ (time, slack) |
37 Played time => Time.+ (time, slack) |
38 | _ => preplay_timeout) |
38 | _ => preplay_timeout) |
39 |
39 |
40 fun try_method meth = |
40 fun try_method meth = |
41 (case preplay_isar_step ctxt timeout meth step of |
41 (case preplay_isar_step ctxt timeout meth step of |