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