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