# HG changeset patch
# User wenzelm
# Date 1158599566 -7200
# Node ID a10885a269cb762d29aa71eb2fbbc832c0e37e16
# Parent  c945a208e7f8a9e8021504f8f0866ebd88e8840a
added class_deps;

diff -r c945a208e7f8 -r a10885a269cb src/Pure/Isar/isar_cmd.ML
--- 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 *)
 
diff -r c945a208e7f8 -r a10885a269cb src/Pure/Isar/isar_syn.ML
--- 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,