# HG changeset patch
# User haftmann
# Date 1421862000 -3600
# Node ID ef1edfb36af7e9799b5eca600bdc39b2e3f79dc7
# Parent  2fb2194853cccc4f0d5e7462469e957c08878ff4
option for formally inlined class specifications in hierarchy graph

diff -r 2fb2194853cc -r ef1edfb36af7 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Jan 21 17:27:58 2015 +0100
+++ b/src/Pure/Isar/class.ML	Wed Jan 21 18:40:00 2015 +0100
@@ -51,7 +51,7 @@
   val default_intro_tac: Proof.context -> thm list -> tactic
 
   (*diagnostics*)
-  val pretty_specification: theory -> class -> Pretty.T list
+  val pretty_specification: theory -> class -> Pretty.T list * Pretty.T list
 end;
 
 structure Class: CLASS =
@@ -750,8 +750,8 @@
         else
           maps (Element.pretty_ctxt_no_attribs class_ctxt) (fixes @ assumes)
           |> maps (fn prt => [Pretty.fbrk, prt]);
-    in if null body then [] else [Pretty.block (header @ body)] end
-  else [];
+    in (header, body) end
+  else ([], []);
 
 end;
 
diff -r 2fb2194853cc -r ef1edfb36af7 src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Wed Jan 21 17:27:58 2015 +0100
+++ b/src/Pure/Tools/class_deps.ML	Wed Jan 21 18:40:00 2015 +0100
@@ -6,6 +6,7 @@
 
 signature CLASS_DEPS =
 sig
+  val inlined_class_specs: bool Config.T
   val class_deps: Proof.context -> sort -> sort option -> unit
   val class_deps_cmd: Proof.context -> string -> string option -> unit
 end;
@@ -13,6 +14,10 @@
 structure Class_Deps: CLASS_DEPS =
 struct
 
+val inlined_class_specs = Attrib.setup_config_bool @{binding "inlined_class_specs"} (K false);
+
+val stringify = XML.content_of o YXML.parse_body o Pretty.string_of;
+
 fun gen_class_deps prep_sort ctxt raw_super raw_sub =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -27,9 +32,23 @@
     val (_, algebra) =
       Sorts.subalgebra (Context.pretty ctxt)
         (le_super andf sub_le) (K NONE) original_algebra;
-    fun node c =
-      Graph_Display.content_node (Name_Space.extern ctxt space c)
-        (Class.pretty_specification thy c);
+    val inlined = Config.get ctxt inlined_class_specs;
+    fun label_for c =
+      if inlined
+      then (stringify o Pretty.block o op @) (Class.pretty_specification thy c)
+      else Name_Space.extern ctxt space c;
+    fun tooltip_for c =
+      if inlined
+      then []
+      else
+        let
+          val pretty_spec = Class.pretty_specification thy c
+        in
+          if (null o snd) pretty_spec
+          then []
+          else [(Pretty.block o op @) pretty_spec]
+        end;
+    fun node c = Graph_Display.content_node (label_for c) (tooltip_for c);
   in
     Sorts.classes_of algebra
     |> Graph.dest