equal
deleted
inserted
replaced
141 val _ = name = "" andalso error ("Bad file name: " ^ quote file); |
141 val _ = name = "" andalso error ("Bad file name: " ^ quote file); |
142 val _ = |
142 val _ = |
143 if ThyInfo.check_known_thy name then |
143 if ThyInfo.check_known_thy name then |
144 (Isar.commit_exit (); ThyInfo.touch_child_thys name; ThyInfo.register_thy name) |
144 (Isar.commit_exit (); ThyInfo.touch_child_thys name; ThyInfo.register_thy name) |
145 handle ERROR msg => |
145 handle ERROR msg => |
146 (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]); |
146 (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]); |
147 tell_file_retracted (ThyLoad.thy_path name)) |
147 tell_file_retracted (ThyLoad.thy_path name)) |
148 else (); |
148 else (); |
149 val _ = Isar.init_point (); |
149 val _ = Isar.init_point (); |
150 in () end; |
150 in () end; |
151 |
151 |