equal
deleted
inserted
replaced
127 fun interp_gain timeout thy file = |
127 fun interp_gain timeout thy file = |
128 let |
128 let |
129 val t1 = (parse_timed file |> fst) |
129 val t1 = (parse_timed file |> fst) |
130 val t2 = (interpret_timed timeout file thy |> fst) |
130 val t2 = (interpret_timed timeout file thy |> fst) |
131 handle exn => (*FIXME*) |
131 handle exn => (*FIXME*) |
132 if Exn.is_interrupt exn then reraise exn |
132 if Exn.is_interrupt exn then Exn.reraise exn |
133 else |
133 else |
134 (warning (" test: file " ^ Path.print file ^ |
134 (warning (" test: file " ^ Path.print file ^ |
135 " raised exception: " ^ Runtime.exn_message exn); |
135 " raised exception: " ^ Runtime.exn_message exn); |
136 {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime}) |
136 {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime}) |
137 val to_real = Time.toReal |
137 val to_real = Time.toReal |