# HG changeset patch
# User wenzelm
# Date 1430667714 -7200
# Node ID 523ec7e4b02283c9b5bbaf2dd45653cc3c22bd60
# Parent  5901cb4db0ae1f8501c9e3f4af9cb031a5ccf1a8
tuned output;

diff -r 5901cb4db0ae -r 523ec7e4b022 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sun May 03 17:36:46 2015 +0200
+++ b/src/Pure/Isar/named_target.ML	Sun May 03 17:41:54 2015 +0200
@@ -116,28 +116,28 @@
 (* pretty *)
 
 fun pretty (target, is_class) ctxt =
-  let
-    val target_name =
-      [Pretty.keyword1 (if is_class then "class" else "locale"), Pretty.brk 1,
-        Locale.pretty_name ctxt target];
-    val fixes =
-      map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
-        (#1 (Proof_Context.inferred_fixes ctxt));
-    val assumes =
-      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
-        (Assumption.all_assms_of ctxt);
-    val elems =
-      (if null fixes then [] else [Element.Fixes fixes]) @
-      (if null assumes then [] else [Element.Assumes assumes]);
-    val body_elems =
-      if target = "" then []
-      else if null elems then [Pretty.block target_name]
+  if target = "" then
+    [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
+      Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]
+  else if is_class then Class.pretty_specification (Proof_Context.theory_of ctxt) target
+  else
+    (* FIXME pretty locale content *)
+    let
+      val target_name = [Pretty.keyword1 "locale", Pretty.brk 1, Locale.pretty_name ctxt target];
+      val fixes =
+        map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
+          (#1 (Proof_Context.inferred_fixes ctxt));
+      val assumes =
+        map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
+          (Assumption.all_assms_of ctxt);
+      val elems =
+        (if null fixes then [] else [Element.Fixes fixes]) @
+        (if null assumes then [] else [Element.Assumes assumes]);
+    in
+      if null elems then [Pretty.block target_name]
       else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
-        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
-  in
-    Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
-      Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))] :: body_elems
-  end;
+        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
+    end;
 
 
 (* init *)