60093
|
1 |
(* Title: Pure/Tools/thy_deps.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Visualization of theory dependencies.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature THY_DEPS =
|
|
8 |
sig
|
60099
|
9 |
val thy_deps: Proof.context -> theory list option * theory list option -> Graph_Display.entry list
|
|
10 |
val thy_deps_cmd: Proof.context ->
|
|
11 |
(string * Position.T) list option * (string * Position.T) list option -> unit
|
60093
|
12 |
end;
|
|
13 |
|
|
14 |
structure Thy_Deps: THY_DEPS =
|
|
15 |
struct
|
|
16 |
|
60099
|
17 |
fun gen_thy_deps _ ctxt (NONE, NONE) =
|
60093
|
18 |
let
|
|
19 |
val parent_session = Session.get_name ();
|
|
20 |
val parent_loaded = is_some o Thy_Info.lookup_theory;
|
60099
|
21 |
in Present.session_graph parent_session parent_loaded (Proof_Context.theory_of ctxt) end
|
|
22 |
| gen_thy_deps prep_thy ctxt bounds =
|
60093
|
23 |
let
|
60099
|
24 |
val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
|
60948
|
25 |
val rel = Context.subthy o swap;
|
60093
|
26 |
val pred =
|
|
27 |
(case upper of
|
|
28 |
SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs)
|
|
29 |
| NONE => K true) andf
|
|
30 |
(case lower of
|
|
31 |
SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
|
|
32 |
| NONE => K true);
|
|
33 |
fun node thy =
|
|
34 |
((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
|
|
35 |
map Context.theory_name (filter pred (Theory.parents_of thy)));
|
60099
|
36 |
in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
|
60093
|
37 |
|
60099
|
38 |
val thy_deps =
|
|
39 |
gen_thy_deps (fn ctxt => fn thy =>
|
|
40 |
let val thy0 = Proof_Context.theory_of ctxt
|
60948
|
41 |
in if Context.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end);
|
60099
|
42 |
|
|
43 |
val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Theory.check;
|
60093
|
44 |
|
|
45 |
end;
|