111 (* theory loader actions *) |
111 (* theory loader actions *) |
112 |
112 |
113 local |
113 local |
114 |
114 |
115 fun trace_action action name = |
115 fun trace_action action name = |
116 if action = ThyInfo.Update then |
116 if action = Thy_Info.Update then |
117 List.app tell_file_loaded (ThyInfo.loaded_files name) |
117 List.app tell_file_loaded (Thy_Info.loaded_files name) |
118 else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then |
118 else if action = Thy_Info.Outdate orelse action = Thy_Info.Remove then |
119 List.app tell_file_retracted (ThyInfo.loaded_files name) |
119 List.app tell_file_retracted (Thy_Info.loaded_files name) |
120 else (); |
120 else (); |
121 |
121 |
122 in |
122 in |
123 fun setup_thy_loader () = ThyInfo.add_hook trace_action; |
123 fun setup_thy_loader () = Thy_Info.add_hook trace_action; |
124 fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ()); |
124 fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ()); |
125 end; |
125 end; |
126 |
126 |
127 |
127 |
128 (* get informed about files *) |
128 (* get informed about files *) |
129 |
129 |
130 (*liberal low-level version*) |
130 (*liberal low-level version*) |
131 val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/"; |
131 val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/"; |
132 |
132 |
133 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name; |
133 val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name; |
134 |
134 |
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 ThyInfo.check_known_thy name then |
140 if Thy_Info.check_known_thy name then |
141 (Isar.>> (Toplevel.commit_exit Position.none); |
141 (Isar.>> (Toplevel.commit_exit Position.none); |
142 ThyInfo.touch_child_thys name; ThyInfo.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 (ThyLoad.thy_path name)) |
145 tell_file_retracted (Thy_Load.thy_path name)) |
146 else (); |
146 else (); |
147 val _ = Isar.init (); |
147 val _ = Isar.init (); |
148 in () end; |
148 in () end; |
149 |
149 |
150 |
150 |