equal
deleted
inserted
replaced
66 local |
66 local |
67 open Unsynchronized |
67 open Unsynchronized |
68 val metis_fail = ref false |
68 val metis_fail = ref false |
69 in |
69 in |
70 fun handle_metis_fail try_metis () = |
70 fun handle_metis_fail try_metis () = |
71 try_metis () handle exp => |
71 try_metis () handle exn => |
72 (if Exn.is_interrupt exp orelse debug then reraise exp |
72 (if Exn.is_interrupt exn orelse debug then reraise exn |
73 else metis_fail := true; SOME Time.zeroTime) |
73 else metis_fail := true; SOME Time.zeroTime) |
74 fun get_time lazy_time = |
74 fun get_time lazy_time = |
75 if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time |
75 if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time |
76 val metis_fail = fn () => !metis_fail |
76 val metis_fail = fn () => !metis_fail |
77 end |
77 end |