142 |
143 |
143 (*Change thy_info and ml_info for an existent item or create |
144 (*Change thy_info and ml_info for an existent item or create |
144 a new item with empty child list *) |
145 a new item with empty child list *) |
145 fun set_info thy_new ml_new thy = |
146 fun set_info thy_new ml_new thy = |
146 let fun make_change (t :: loaded) = |
147 let fun make_change (t :: loaded) = |
147 let val ThyInfo {name, childs, theory, ...} = t |
148 let val ThyInfo {name, children, theory, ...} = t |
148 in if name = thy then |
149 in if name = thy then |
149 ThyInfo {name = name, childs = childs, |
150 ThyInfo {name = name, children = children, |
150 thy_info = thy_new, ml_info = ml_new, |
151 thy_info = thy_new, ml_info = ml_new, |
151 theory = theory} :: loaded |
152 theory = theory} :: loaded |
152 else |
153 else |
153 t :: (make_change loaded) |
154 t :: (make_change loaded) |
154 end |
155 end |
155 | make_change [] = raise THY_NOT_FOUND |
156 | make_change [] = raise THY_NOT_FOUND |
156 in loaded_thys := make_change (!loaded_thys) end; |
157 in loaded_thys := make_change (!loaded_thys) end; |
157 |
158 |
158 (*Mark all direct and indirect descendants of a theory as changed *) |
159 (*Mark all direct and indirect descendants of a theory as changed *) |
159 fun mark_childs thy = |
160 fun mark_children thy = |
160 let val ThyInfo {childs, ...} = get_thyinfo thy |
161 let val ThyInfo {children, ...} = get_thyinfo thy |
161 in writeln ("Marking childs of modified theory " ^ thy ^ " (" ^ |
162 in if children <> [] then |
162 (space_implode "," childs) ^ ")"); |
163 (writeln ("The following children of theory " ^ (quote thy) |
163 seq (set_info "" "") childs |
164 ^ " are now out-of-date: \"" |
164 handle THY_NOT_FOUND => () |
165 ^ (space_implode "\",\"" children) ^ "\""); |
|
166 seq (set_info "" "") children |
|
167 handle THY_NOT_FOUND => () |
165 (*If this theory was automatically loaded by a child |
168 (*If this theory was automatically loaded by a child |
166 then the child cannot be found in loaded_thys *) |
169 then the child cannot be found in loaded_thys *) |
|
170 ) |
|
171 else () |
167 end |
172 end |
168 |
173 |
169 in if thy_uptodate andalso ml_uptodate then () |
174 in if thy_uptodate andalso ml_uptodate then () |
170 else |
175 else |
171 ( |
176 ( |
172 writeln ("Loading theory " ^ name); |
177 writeln ("Loading theory " ^ (quote name)); |
173 if thy_uptodate orelse (thy_file = "") then () |
178 if thy_uptodate orelse (thy_file = "") then () |
174 else |
179 else |
175 ( |
180 ( |
176 (*Allow dependency lists to be rebuild completely *) |
181 (*Allow dependency lists to be rebuild completely *) |
177 remove_child thy; |
182 remove_child thy; |
252 | reload_changed [] = () |
258 | reload_changed [] = () |
253 in reload_changed (load_order ["pure"] []) end; |
259 in reload_changed (load_order ["pure"] []) end; |
254 |
260 |
255 (*Merge theories to build a base for a new theory. |
261 (*Merge theories to build a base for a new theory. |
256 Base members are only loaded if they are missing. *) |
262 Base members are only loaded if they are missing. *) |
257 fun base_on (t :: ts) child = |
263 fun base_on bases child = |
258 let val childl = to_lower child; |
264 let val childl = to_lower child; |
259 |
265 |
260 fun load_base base = |
266 (*List all descendants of a theory list *) |
261 let val basel = to_lower base; |
267 fun list_descendants (t :: ts) = |
262 |
268 if already_loaded t then |
263 (*List all descendants of a theory list *) |
269 let val ThyInfo {children, ...} = get_thyinfo t |
264 fun list_descendants (t :: ts) = |
270 in children union |
265 if already_loaded t then |
271 (list_descendants (ts union children)) |
266 let val ThyInfo {childs, ...} = get_thyinfo t |
272 end |
267 in childs union (list_descendants (ts union childs)) |
273 else [] |
268 end |
274 | list_descendants [] = []; |
269 else [] |
275 |
270 | list_descendants [] = []; |
276 (*Show the cycle that would be created by add_child *) |
271 |
277 fun show_cycle base = |
272 (*Show the cycle that would be created by add_child *) |
278 let fun find_it result curr = |
273 fun show_cycle () = |
279 if base = curr then |
274 let fun find_it result curr = |
280 error ("Cyclic dependency of theories: " |
275 if basel = curr then |
281 ^ childl ^ "->" ^ base ^ result) |
276 error ("Cyclic dependency of theories: " |
282 else if already_loaded curr then |
277 ^ childl ^ "->" ^ basel ^ result) |
283 let val ThyInfo {children, ...} = get_thyinfo curr |
278 else if already_loaded curr then |
284 in seq (find_it ("->" ^ curr ^ result)) children |
279 let val ThyInfo {childs, ...} = get_thyinfo curr |
285 end |
280 in seq (find_it ("->" ^ curr ^ result)) childs |
286 else () |
281 end |
287 in find_it "" childl end; |
282 else () |
288 |
283 in find_it "" childl end; |
289 (*Check if a cycle will be created by add_child *) |
284 |
290 fun find_cycle base = |
285 (*Check if a cycle will be created by add_child *) |
291 if base mem (list_descendants [childl]) then show_cycle base |
286 fun find_cycle () = |
292 else (); |
287 if basel mem (list_descendants [childl]) then show_cycle () |
|
288 else (); |
|
289 |
293 |
290 (*Add child to child list of base *) |
294 (*Add child to child list of base *) |
291 fun add_child (t :: loaded) = |
295 fun add_child (t :: loaded) base = |
292 let val ThyInfo {name, childs, thy_info, ml_info, |
296 let val ThyInfo {name, children, thy_info, ml_info, theory} = t |
293 theory} = t |
297 in if name = base then |
294 in if name = basel then |
298 ThyInfo {name = name, |
295 ThyInfo {name = name, childs = childl ins childs, |
299 children = childl ins children, |
296 thy_info = thy_info, ml_info = ml_info, |
300 thy_info = thy_info, ml_info = ml_info, |
297 theory = theory} :: loaded |
301 theory = theory} :: loaded |
298 else |
302 else |
299 t :: (add_child loaded) |
303 t :: (add_child loaded base) |
300 end |
304 end |
301 | add_child [] = |
305 | add_child [] base = |
302 [ThyInfo {name = basel, childs = [childl], |
306 [ThyInfo {name = base, children = [childl], |
303 thy_info = "", ml_info = "", |
307 thy_info = "", ml_info = "", |
304 theory = Thm.pure_thy}]; |
308 theory = Thm.pure_thy}]; |
305 (*Thm.pure_thy is used as a dummy *) |
309 (*Thm.pure_thy is used as a dummy *) |
306 |
310 |
307 val thy_there = already_loaded basel |
311 fun do_load thy = |
|
312 let val basel = to_lower thy; |
|
313 |
|
314 val thy_present = already_loaded basel |
308 (*test this before child is added *) |
315 (*test this before child is added *) |
309 in |
316 in |
310 if childl = basel then |
317 if childl = basel then |
311 error ("Cyclic dependency of theories: " ^ child |
318 error ("Cyclic dependency of theories: " ^ child |
312 ^ "->" ^ child) |
319 ^ "->" ^ child) |
313 else find_cycle (); |
320 else |
314 loaded_thys := add_child (!loaded_thys); |
321 (find_cycle thy; |
315 if thy_there then () |
322 loaded_thys := add_child (!loaded_thys) basel; |
316 else (writeln ("Autoloading theory " ^ base |
323 if thy_present then () |
317 ^ " (used by " ^ child ^ ")"); |
324 else (writeln ("Autoloading theory " ^ (quote thy) |
318 use_thy base |
325 ^ " (used by " ^ (quote child) ^ ")"); |
319 ) |
326 use_thy thy) |
320 end; |
327 ) |
|
328 end; |
|
329 |
|
330 fun load_base (Thy b :: bs) = |
|
331 (do_load b; |
|
332 (to_lower b) :: (load_base bs)) |
|
333 | load_base (File b :: bs) = |
|
334 (do_load b; |
|
335 load_base bs) (*don't add it to merge_theories' parameter *) |
|
336 | load_base [] = []; |
321 |
337 |
322 val (tl :: tls) = map to_lower (t :: ts) |
338 val (t :: ts) = load_base bases |
323 in seq load_base (t :: ts); |
339 in foldl Thm.merge_theories (get_theory t, map get_theory ts) end; |
324 foldl Thm.merge_theories (get_theory tl, map get_theory tls) |
|
325 end |
|
326 | base_on [] _ = raise Match; |
|
327 |
340 |
328 (*Change theory object for an existent item of loaded_thys |
341 (*Change theory object for an existent item of loaded_thys |
329 or create a new item *) |
342 or create a new item *) |
330 fun store_theory thy_name thy = |
343 fun store_theory thy_name thy = |
331 let fun make_change (t :: loaded) = |
344 let fun make_change (t :: loaded) = |
332 let val ThyInfo {name, childs, thy_info, ml_info, ...} = t |
345 let val ThyInfo {name, children, thy_info, ml_info, ...} = t |
333 in if name = (to_lower thy_name) then |
346 in if name = (to_lower thy_name) then |
334 ThyInfo {name = name, childs = childs, |
347 ThyInfo {name = name, children = children, |
335 thy_info = thy_info, ml_info = ml_info, |
348 thy_info = thy_info, ml_info = ml_info, |
336 theory = thy} :: loaded |
349 theory = thy} :: loaded |
337 else |
350 else |
338 t :: (make_change loaded) |
351 t :: (make_change loaded) |
339 end |
352 end |
340 | make_change [] = |
353 | make_change [] = |
341 [ThyInfo {name = (to_lower thy_name), childs = [], thy_info = "", |
354 [ThyInfo {name = (to_lower thy_name), children = [], thy_info = "", |
342 ml_info = "", theory = thy}] |
355 ml_info = "", theory = thy}] |
343 in loaded_thys := make_change (!loaded_thys) end; |
356 in loaded_thys := make_change (!loaded_thys) end; |
344 |
357 |
345 (*Create a list of all theories loaded by this structure *) |
358 (*Create a list of all theories loaded by this structure *) |
346 fun list_loaded () = (!loaded_thys); |
359 fun list_loaded () = (!loaded_thys); |
347 |
360 |
348 (*Change the list of loaded theories *) |
361 (*Change the list of loaded theories *) |
349 fun set_loaded [] = |
362 fun set_loaded [] = |
350 loaded_thys := [ThyInfo {name = "pure", childs = [], thy_info = "", |
363 loaded_thys := [ThyInfo {name = "pure", children = [], thy_info = "", |
351 ml_info = "", theory = Thm.pure_thy}] |
364 ml_info = "", theory = Thm.pure_thy}] |
352 | set_loaded ts = |
365 | set_loaded ts = |
353 loaded_thys := ts; |
366 loaded_thys := ts; |
354 |
367 |
355 (*Change the path list that is to be searched for .thy and .ML files *) |
368 (*Change the path list that is to be searched for .thy and .ML files *) |
356 fun set_loadpath new_path = |
369 fun set_loadpath new_path = |
357 loadpath := new_path; |
370 loadpath := new_path; |
358 |
371 |
359 (*This function is for debugging purposes only *) |
372 (*This function is for debugging purposes only *) |
360 fun relations thy = |
373 fun relations thy = |
361 let val ThyInfo {childs, ...} = get_thyinfo thy |
374 let val ThyInfo {children, ...} = get_thyinfo thy |
362 in |
375 in |
363 writeln (thy ^ ": " ^ (space_implode ", " childs)); |
376 writeln (thy ^ ": " ^ (space_implode ", " children)); |
364 seq relations childs |
377 seq relations children |
365 end |
378 end |
366 |
379 |
367 end; |
380 end; |
368 |
381 |