equal
deleted
inserted
replaced
196 |
196 |
197 fun reset_state tr st0 = Toplevel.setmp_thread_position tr (fn () => |
197 fun reset_state tr st0 = Toplevel.setmp_thread_position tr (fn () => |
198 let |
198 let |
199 val name = Toplevel.name_of tr; |
199 val name = Toplevel.name_of tr; |
200 val res = |
200 val res = |
201 if Keyword.is_theory name andalso not (Keyword.is_theory_begin name) then |
201 if Keyword.is_theory_body name then Toplevel.reset_theory st0 |
202 Toplevel.reset_theory st0 |
202 else if Keyword.is_proof name then Toplevel.reset_proof st0 |
203 else if Keyword.is_proof name then |
|
204 Toplevel.reset_proof st0 |
|
205 else NONE; |
203 else NONE; |
206 in |
204 in |
207 (case res of |
205 (case res of |
208 NONE => st0 |
206 NONE => st0 |
209 | SOME st => (warning (Toplevel.type_error tr st0 ^ " -- resetting state"); st)) |
207 | SOME st => (warning (Toplevel.type_error tr st0 ^ " -- resetting state"); st)) |