# HG changeset patch
# User wenzelm
# Date 1421509210 -3600
# Node ID 1434ef1e0ede84f6f81360f5bfcbd40d0d47a581
# Parent  a78e71fcd1465e89334454affd75bbf2a64de76e
clarified Class.pretty_specification: imitate input source;

diff -r a78e71fcd146 -r 1434ef1e0ede src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Jan 16 23:24:29 2015 +0100
+++ b/src/Pure/Isar/class.ML	Sat Jan 17 16:40:10 2015 +0100
@@ -51,7 +51,7 @@
   val default_intro_tac: Proof.context -> thm list -> tactic
 
   (*diagnostics*)
-  val pretty_body: theory -> class -> Pretty.T list
+  val pretty_specification: theory -> class -> Pretty.T list
 end;
 
 structure Class: CLASS =
@@ -731,12 +731,25 @@
 
 (** diagnostics **)
 
-fun pretty_body thy c =
-  let
-    val cs = (#params o Axclass.get_info thy) c;
-    val fix_args = map (fn (c, T) => ((Binding.name o Long_Name.base_name) c, SOME T, NoSyn)) cs; 
-    val fixes = if null fix_args then [] else [Element.Fixes fix_args];
-  in maps (Element.pretty_ctxt (init c thy)) (fixes @ Locale.hyp_spec_of thy c) end;
+fun pretty_specification thy c =
+  if is_class thy c then
+    let
+      val class_ctxt = init c thy;
+      val class_space = Proof_Context.class_space class_ctxt;
+
+      val fix_args =
+        #params (Axclass.get_info thy c)
+        |> map (fn (c, T) => (Binding.name (Long_Name.base_name c), SOME T, NoSyn));
+      val fixes = if null fix_args then [] else [Element.Fixes fix_args];
+      val assumes = Locale.hyp_spec_of thy c;
+
+      val header =
+        [Pretty.keyword1 "class", Pretty.brk 1, Name_Space.pretty class_ctxt class_space c];
+      val body =
+        maps (Element.pretty_ctxt class_ctxt) (fixes @ assumes)
+        |> maps (fn prt => [Pretty.fbrk, prt]);
+    in [Pretty.block (header @ body)] end
+  else [];
 
 end;
 
diff -r a78e71fcd146 -r 1434ef1e0ede src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Fri Jan 16 23:24:29 2015 +0100
+++ b/src/Pure/Tools/class_deps.ML	Sat Jan 17 16:40:10 2015 +0100
@@ -27,12 +27,13 @@
     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 [];
+    fun node c =
+      Graph_Display.content_node (Name_Space.extern ctxt space c)
+        (Class.pretty_specification thy c);
   in
     Sorts.classes_of algebra
     |> Graph.dest
-    |> map (fn ((c, _), ds) =>
-        ((c, Graph_Display.content_node (Name_Space.extern ctxt space c) (pretty_body_of c)), ds))
+    |> map (fn ((c, _), ds) => ((c, node c), ds))
     |> Graph_Display.display_graph
   end;