# HG changeset patch
# User haftmann
# Date 1410105088 -7200
# Node ID 5bf56c758e021c6e9594deece55e9be768df6f70
# Parent  d95055489fce4febed663838d4af7702d92fc0d3
separated class_deps command into separate file

diff -r d95055489fce -r 5bf56c758e02 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Sep 07 14:39:23 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Sep 07 17:51:28 2014 +0200
@@ -38,7 +38,6 @@
   val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
   val thy_deps: Toplevel.transition -> Toplevel.transition
   val locale_deps: Toplevel.transition -> Toplevel.transition
-  val class_deps: Toplevel.transition -> Toplevel.transition
   val print_stmts: string list * (Facts.ref * Token.src list) list
     -> Toplevel.transition -> Toplevel.transition
   val print_thms: string list * (Facts.ref * Token.src list) list
@@ -298,19 +297,6 @@
       dir = "", unfold = true, path = "", content = [body]});
   in Graph_Display.display_graph gr end);
 
-val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  let
-    val ctxt = Toplevel.context_of state;
-    val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
-    val classes = Sorts.classes_of algebra;
-    fun entry (c, (i, (_, cs))) =
-      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
-            dir = "", unfold = true, path = "", content = []});
-    val gr =
-      Graph.fold (cons o entry) classes []
-      |> sort (int_ord o pairself #1) |> map #2;
-  in Graph_Display.display_graph gr end);
-
 
 (* print theorems, terms, types etc. *)
 
diff -r d95055489fce -r 5bf56c758e02 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Sep 07 14:39:23 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Sep 07 17:51:28 2014 +0200
@@ -890,10 +890,6 @@
     (Scan.succeed Isar_Cmd.locale_deps);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
-    (Scan.succeed Isar_Cmd.class_deps);
-
-val _ =
   Outer_Syntax.improper_command @{command_spec "print_binds"}
     "print term bindings of proof context -- Proof General legacy"
     (Scan.succeed (Toplevel.unknown_context o
diff -r d95055489fce -r 5bf56c758e02 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Sep 07 14:39:23 2014 +0200
+++ b/src/Pure/Pure.thy	Sun Sep 07 17:51:28 2014 +0200
@@ -113,6 +113,7 @@
 ML_file "Tools/rail.ML"
 ML_file "Tools/rule_insts.ML";
 ML_file "Tools/thm_deps.ML";
+ML_file "Tools/class_deps.ML"
 ML_file "Tools/find_theorems.ML"
 ML_file "Tools/find_consts.ML"
 ML_file "Tools/proof_general_pure.ML"
diff -r d95055489fce -r 5bf56c758e02 src/Pure/Tools/class_deps.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/class_deps.ML	Sun Sep 07 17:51:28 2014 +0200
@@ -0,0 +1,32 @@
+(*  Title:      Pure/Tools/class_deps.ML
+    Author:     Florian Haftmann, TU Muenchen
+
+Visualization of class dependencies.
+*)
+
+signature CLASS_DEPS =
+sig
+  val class_deps: Toplevel.transition -> Toplevel.transition
+end;
+
+structure Class_deps: CLASS_DEPS =
+struct
+
+val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+  let
+    val ctxt = Toplevel.context_of state;
+    val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
+    val classes = Sorts.classes_of algebra;
+    fun entry (c, (i, (_, cs))) =
+      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
+            dir = "", unfold = true, path = "", content = []});
+    val gr =
+      Graph.fold (cons o entry) classes []
+      |> sort (int_ord o pairself #1) |> map #2;
+  in Graph_Display.display_graph gr end);
+
+val _ =
+  Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
+    (Scan.succeed class_deps);
+
+end;