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