equal
deleted
inserted
replaced
135 fun inform_file_processed file = |
135 fun inform_file_processed file = |
136 let |
136 let |
137 val name = thy_name file; |
137 val name = thy_name file; |
138 val _ = name = "" andalso error ("Bad file name: " ^ quote file); |
138 val _ = name = "" andalso error ("Bad file name: " ^ quote file); |
139 val _ = |
139 val _ = |
140 if Thy_Info.check_known_thy name then |
140 if Thy_Info.known_thy name then |
141 (Isar.>> (Toplevel.commit_exit Position.none); |
141 (Isar.>> (Toplevel.commit_exit Position.none); |
142 Thy_Info.touch_child_thys name; Thy_Info.register_thy name) |
142 Thy_Info.touch_child_thys name; Thy_Info.register_thy name) |
143 handle ERROR msg => |
143 handle ERROR msg => |
144 (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]); |
144 (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]); |
145 tell_file_retracted (Thy_Load.thy_path name)) |
145 tell_file_retracted (Thy_Load.thy_path name)) |