author | wenzelm |
Thu, 16 Apr 2015 15:22:44 +0200 | |
changeset 60097 | d20ca79d50e4 |
parent 60093 | c48d536231fe |
child 60099 | 73c260342704 |
permissions | -rw-r--r-- |
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 |
|
9 |
val thy_deps: theory -> theory list option * theory list option -> Graph_Display.entry list |
|
10 |
val thy_deps_cmd: theory -> string list option * string list option -> unit |
|
11 |
end; |
|
12 |
||
13 |
structure Thy_Deps: THY_DEPS = |
|
14 |
struct |
|
15 |
||
16 |
fun gen_thy_deps _ thy0 (NONE, NONE) = |
|
17 |
let |
|
18 |
val parent_session = Session.get_name (); |
|
19 |
val parent_loaded = is_some o Thy_Info.lookup_theory; |
|
20 |
in Present.session_graph parent_session parent_loaded thy0 end |
|
21 |
| gen_thy_deps prep_thy thy0 bounds = |
|
22 |
let |
|
23 |
val (upper, lower) = apply2 ((Option.map o map) (prep_thy thy0)) bounds; |
|
24 |
val rel = Theory.subthy o swap; |
|
25 |
val pred = |
|
26 |
(case upper of |
|
27 |
SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs) |
|
28 |
| NONE => K true) andf |
|
29 |
(case lower of |
|
30 |
SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs) |
|
31 |
| NONE => K true); |
|
32 |
fun node thy = |
|
33 |
((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []), |
|
34 |
map Context.theory_name (filter pred (Theory.parents_of thy))); |
|
35 |
in Theory.nodes_of thy0 |> filter pred |> map node end; |
|
36 |
||
37 |
val thy_deps = gen_thy_deps (K I); |
|
38 |
val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Context.get_theory; |
|
39 |
||
40 |
val theory_bounds = |
|
41 |
Parse.theory_xname >> single || |
|
42 |
(@{keyword "("} |-- Parse.enum "|" Parse.theory_xname --| @{keyword ")"}); |
|
43 |
||
44 |
val _ = |
|
45 |
Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies" |
|
60097
d20ca79d50e4
discontinued pointless warnings: commands are only defined inside a theory context;
wenzelm
parents:
60093
diff
changeset
|
46 |
(Scan.option theory_bounds -- Scan.option theory_bounds >> |
d20ca79d50e4
discontinued pointless warnings: commands are only defined inside a theory context;
wenzelm
parents:
60093
diff
changeset
|
47 |
(fn args => Toplevel.keep (fn st => thy_deps_cmd (Toplevel.theory_of st) args))); |
60093 | 48 |
|
49 |
end; |