equal
deleted
inserted
replaced
109 |> Proof.map_context (Context_Position.set_visible false) |
109 |> Proof.map_context (Context_Position.set_visible false) |
110 val auto_time_limit = Options.default_real @{system_option auto_time_limit} |
110 val auto_time_limit = Options.default_real @{system_option auto_time_limit} |
111 in |
111 in |
112 if auto_time_limit > 0.0 then |
112 if auto_time_limit > 0.0 then |
113 (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of |
113 (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of |
114 (true, (_, outcome)) => List.app writeln outcome |
114 (true, (_, outcome)) => List.app Output.information outcome |
115 | _ => ()) |
115 | _ => ()) |
116 else () |
116 else () |
117 end handle exn => if Exn.is_interrupt exn then reraise exn else ()} |
117 end handle exn => if Exn.is_interrupt exn then reraise exn else ()} |
118 else NONE) |
118 else NONE) |
119 |
119 |