src/Pure/Tools/class_deps.ML
changeset 59296 002d817b4c37
parent 59210 8658b4290aed
child 59301 9089639ba348
--- a/src/Pure/Tools/class_deps.ML	Mon Jan 05 23:33:39 2015 +0100
+++ b/src/Pure/Tools/class_deps.ML	Mon Jan 05 18:39:32 2015 +0100
@@ -15,6 +15,7 @@
 
 fun gen_visualize prep_sort ctxt raw_super raw_sub =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val super = prep_sort ctxt raw_super;
     val sub = Option.map (prep_sort ctxt) raw_sub;
     val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
@@ -26,11 +27,12 @@
     val (_, algebra) =
       Sorts.subalgebra (Context.pretty ctxt)
         (le_super andf sub_le) (K NONE) original_algebra;
+    fun pretty_body_of c = if Class.is_class thy c then Class.pretty_body thy c else [];
   in
     Sorts.classes_of algebra
     |> Graph.dest
     |> map (fn ((c, _), ds) =>
-        ((c, Graph_Display.content_node (Name_Space.extern ctxt space c) []), ds))
+        ((c, Graph_Display.content_node (Name_Space.extern ctxt space c) (pretty_body_of c)), ds))
     |> Graph_Display.display_graph
   end;