equal
deleted
inserted
replaced
95 (case Toplevel.transition true tr (state ()) of |
95 (case Toplevel.transition true tr (state ()) of |
96 NONE => false |
96 NONE => false |
97 | SOME (_, SOME exn_info) => |
97 | SOME (_, SOME exn_info) => |
98 (set_exn (SOME exn_info); |
98 (set_exn (SOME exn_info); |
99 Toplevel.setmp_thread_position tr |
99 Toplevel.setmp_thread_position tr |
100 ML_Compiler.exn_error_message (Runtime.EXCURSION_FAIL exn_info); |
100 Runtime.exn_error_message (Runtime.EXCURSION_FAIL exn_info); |
101 true) |
101 true) |
102 | SOME (st', NONE) => |
102 | SOME (st', NONE) => |
103 let |
103 let |
104 val name = Toplevel.name_of tr; |
104 val name = Toplevel.name_of tr; |
105 val _ = if Keyword.is_theory_begin name then init () else (); |
105 val _ = if Keyword.is_theory_begin name then init () else (); |
142 in |
142 in |
143 (case Source.get_single (Source.set_prompt Source.default_prompt src) of |
143 (case Source.get_single (Source.set_prompt Source.default_prompt src) of |
144 NONE => if secure then quit () else () |
144 NONE => if secure then quit () else () |
145 | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ()) |
145 | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ()) |
146 handle exn => |
146 handle exn => |
147 (ML_Compiler.exn_error_message exn |
147 (Runtime.exn_error_message exn |
148 handle crash => |
148 handle crash => |
149 (Synchronized.change crashes (cons crash); |
149 (Synchronized.change crashes (cons crash); |
150 warning "Recovering from Isar toplevel crash -- see also Isar.crashes"); |
150 warning "Recovering from Isar toplevel crash -- see also Isar.crashes"); |
151 raw_loop secure src) |
151 raw_loop secure src) |
152 end; |
152 end; |