diff -r bab968955925 -r 002d817b4c37 src/Pure/Tools/class_deps.ML --- 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;