--- a/src/Pure/Isar/isar_cmd.ML Mon Sep 18 19:12:45 2006 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Sep 18 19:12:46 2006 +0200
@@ -57,8 +57,8 @@
val print_trans_rules: Toplevel.transition -> Toplevel.transition
val print_methods: Toplevel.transition -> Toplevel.transition
val print_antiquotations: Toplevel.transition -> Toplevel.transition
- val thm_deps: (thmref * Attrib.src list) list ->
- Toplevel.transition -> Toplevel.transition
+ val class_deps: Toplevel.transition -> Toplevel.transition
+ val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
val find_theorems: int option * (bool * string FindTheorems.criterion) list
-> Toplevel.transition -> Toplevel.transition
val print_binds: Toplevel.transition -> Toplevel.transition
@@ -269,6 +269,19 @@
val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
+val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+ let
+ val thy = Toplevel.theory_of state;
+ val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
+ val {classes, ...} = Sorts.rep_algebra algebra;
+ fun entry (c, (i, (_, cs))) =
+ (i, {name = NameSpace.extern space c, ID = c, parents = cs,
+ dir = "", unfold = true, path = ""});
+ val gr =
+ Graph.fold (cons o entry) classes []
+ |> sort (int_ord o pairself #1) |> map #2;
+ in Present.display_graph gr end);
+
(* retrieve theorems *)
--- a/src/Pure/Isar/isar_syn.ML Mon Sep 18 19:12:45 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Sep 18 19:12:46 2006 +0200
@@ -717,6 +717,10 @@
OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
+val class_depsP =
+ OuterSyntax.improper_command "class_deps" "visualize class dependencies"
+ K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
+
val thm_depsP =
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
@@ -914,10 +918,10 @@
print_syntaxP, print_theoremsP, print_localesP, print_localeP,
print_registrationsP, print_attributesP, print_simpsetP,
print_rulesP, print_induct_rulesP, print_trans_rulesP,
- print_methodsP, print_antiquotationsP, thm_depsP, find_theoremsP,
- print_bindsP, print_lthmsP, print_casesP, print_stmtsP, print_thmsP,
- print_prfsP, print_full_prfsP, print_propP, print_termP,
- print_typeP,
+ print_methodsP, print_antiquotationsP, class_depsP, thm_depsP,
+ find_theoremsP, print_bindsP, print_lthmsP, print_casesP,
+ print_stmtsP, print_thmsP, print_prfsP, print_full_prfsP,
+ print_propP, print_termP, print_typeP,
(*system commands*)
cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,