# HG changeset patch
# User haftmann
# Date 1174402362 -3600
# Node ID 3a7d623485fa0a91687537e7fd08306f5fa6e26c
# Parent  25dfebd7b4c873b026c3ee261d4f8415b75af3df
added theory dependency graph

diff -r 25dfebd7b4c8 -r 3a7d623485fa src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 20 15:52:41 2007 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 20 15:52:42 2007 +0100
@@ -93,6 +93,7 @@
   val print_methods: Toplevel.transition -> Toplevel.transition
   val print_antiquotations: Toplevel.transition -> Toplevel.transition
   val class_deps: Toplevel.transition -> Toplevel.transition
+  val thy_deps: Toplevel.transition -> Toplevel.transition
   val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
   val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
     -> Toplevel.transition -> Toplevel.transition
@@ -490,6 +491,16 @@
 
 val print_antiquotations = Toplevel.imperative ThyOutput.print_antiquotations;
 
+val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+  let
+    val thy = Toplevel.theory_of state;
+    val gr = Theory.dep_graph thy;
+    fun mk_entry (name, ((), (_, parents))) =
+      { name = name, ID = name, dir = "", unfold = true,
+        path = "", parents = parents };
+    val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
+  in Present.display_graph prgr end);
+
 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let
     val thy = Toplevel.theory_of state;
diff -r 25dfebd7b4c8 -r 3a7d623485fa src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Mar 20 15:52:41 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 20 15:52:42 2007 +0100
@@ -790,6 +790,10 @@
   OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
 
+val thy_depsP =
+  OuterSyntax.improper_command "thy_deps" "visualize theory dependencies"
+    K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
+
 val class_depsP =
   OuterSyntax.improper_command "class_deps" "visualize class dependencies"
     K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
@@ -996,7 +1000,7 @@
   print_theoremsP, print_localesP, print_localeP,
   print_registrationsP, print_attributesP, print_simpsetP,
   print_rulesP, print_induct_rulesP, print_trans_rulesP,
-  print_methodsP, print_antiquotationsP, class_depsP, thm_depsP,
+  print_methodsP, print_antiquotationsP, thy_depsP, class_depsP, thm_depsP,
   find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
   print_thmsP, print_prfsP, print_full_prfsP, print_propP,
   print_termP, print_typeP,
diff -r 25dfebd7b4c8 -r 3a7d623485fa src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Mar 20 15:52:41 2007 +0100
+++ b/src/Pure/theory.ML	Tue Mar 20 15:52:42 2007 +0100
@@ -52,6 +52,7 @@
   val add_finals: bool -> string list -> theory -> theory
   val add_finals_i: bool -> term list -> theory -> theory
   val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
+  val dep_graph: theory -> unit Graph.T;
 end
 
 structure Theory: THEORY =
@@ -332,6 +333,25 @@
   NameSpace.extend_table (Sign.naming_of thy) (oracles, [(bname, (oracle, stamp ()))])
     handle Symtab.DUPS dups => err_dup_oras dups);
 
+
+
+(** graph of theory parents **)
+
+fun dep_graph thy =
+  let
+    fun add_thy thy gr =
+      let
+        val name = Context.theory_name thy;
+      in if can (Graph.get_node gr) name then (name, gr)
+      else
+        gr
+        |> Graph.new_node (name, ())
+        |> fold_map add_thy (parents_of thy)
+        |-> (fn names => fold (fn name' => Graph.add_edge (name, name')) names)
+        |> pair name
+      end;
+  in snd (add_thy thy Graph.empty) end;
+
 end;
 
 structure BasicTheory: BASIC_THEORY = Theory;