changeset 73383 | 6b104dc069de |
parent 72584 | 4ea19e5dc67e |
child 75123 | 66eb6fdfc244 |
73382:2b1b7b58d0e7 | 73383:6b104dc069de |
---|---|
55 if timeout <= min_timeout then |
55 if timeout <= min_timeout then |
56 NONE |
56 NONE |
57 else |
57 else |
58 let val y = f timeout x in |
58 let val y = f timeout x in |
59 (case get_time y of |
59 (case get_time y of |
60 SOME time => next_timeout := time_min (time, !next_timeout) |
60 SOME time => next_timeout := Time.min (time, !next_timeout) |
61 | _ => ()); |
61 | _ => ()); |
62 SOME y |
62 SOME y |
63 end |
63 end |
64 end |
64 end |
65 in |
65 in |