# HG changeset patch
# User wenzelm
# Date 1430666367 -7200
# Node ID 3a8501876dbaca070f278c482f1f4466a9312e34
# Parent  cde717a55db7cdfa79c3951acc1f378a5ac9b67f
tuned output -- avoid empty quites and extra breaks;

diff -r cde717a55db7 -r 3a8501876dba src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun May 03 16:45:07 2015 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun May 03 17:19:27 2015 +0200
@@ -18,6 +18,7 @@
   val check_name: Proof.context -> xstring * Position.T -> string
   val check_src: Proof.context -> Token.src -> Token.src
   val pretty_attribs: Proof.context -> Token.src list -> Pretty.T list
+  val pretty_binding: Proof.context -> binding -> string -> Pretty.T list
   val attribute: Proof.context -> Token.src -> attribute
   val attribute_global: theory -> Token.src -> attribute
   val attribute_cmd: Proof.context -> Token.src -> attribute
@@ -158,6 +159,13 @@
 fun pretty_attribs _ [] = []
   | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)];
 
+fun pretty_binding ctxt (b, atts) sep =
+  if is_empty_binding (b, atts) then []
+  else if Binding.is_empty b then
+    [Pretty.block (pretty_attribs ctxt atts @ [Pretty.str sep])]
+  else
+    [Pretty.block (Binding.pretty b :: Pretty.brk 1 :: pretty_attribs ctxt atts @ [Pretty.str sep])];
+
 
 (* get attributes *)
 
diff -r cde717a55db7 -r 3a8501876dba src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun May 03 16:45:07 2015 +0200
+++ b/src/Pure/Isar/element.ML	Sun May 03 17:19:27 2015 +0200
@@ -112,12 +112,6 @@
       Pretty.block [Pretty.keyword2 keyword, Pretty.brk 1, x] ::
         map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword2 sep, Pretty.brk 1, y]) ys;
 
-fun pretty_name_atts ctxt (b, atts) sep =
-  if Attrib.is_empty_binding (b, atts) then []
-  else
-    [Pretty.block (Pretty.breaks
-      (Binding.pretty b :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
-
 
 (* pretty_stmt *)
 
@@ -126,10 +120,10 @@
     val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     val prt_terms = separate (Pretty.keyword2 "and") o map prt_term;
-    val prt_name_atts = pretty_name_atts ctxt;
+    val prt_binding = Attrib.pretty_binding ctxt;
 
     fun prt_show (a, ts) =
-      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
+      Pretty.block (Pretty.breaks (prt_binding a ":" @ prt_terms (map fst ts)));
 
     fun prt_var (x, SOME T) = Pretty.block
           [Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
@@ -153,10 +147,8 @@
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
 
-    fun prt_name_atts (b, atts) sep =
-      if not show_attribs orelse null atts then
-        [Pretty.block [Binding.pretty b, Pretty.str sep]]
-      else pretty_name_atts ctxt (b, atts) sep;
+    fun prt_binding (b, atts) =
+      Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
 
     fun prt_fact (ths, atts) =
       if not show_attribs orelse null atts then map prt_thm ths
@@ -174,12 +166,12 @@
     fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
 
     fun prt_asm (a, ts) =
-      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
+      Pretty.block (Pretty.breaks (prt_binding a ":" @ map (prt_term o fst) ts));
     fun prt_def (a, (t, _)) =
-      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ [prt_term t]));
+      Pretty.block (Pretty.breaks (prt_binding a ":" @ [prt_term t]));
 
     fun prt_note (a, ths) =
-      Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths)));
+      Pretty.block (Pretty.breaks (flat (prt_binding a " =" :: map prt_fact ths)));
   in
     fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes)
      | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs)
diff -r cde717a55db7 -r 3a8501876dba src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun May 03 16:45:07 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun May 03 17:19:27 2015 +0200
@@ -1346,9 +1346,10 @@
       [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1,
         Pretty.quote (prt_term t)];
 
-    fun prt_asm (b, ts) = Pretty.block (Pretty.breaks
-      ((if Binding.is_empty b then []
-        else [Binding.pretty b, Pretty.str ":"]) @ map (Pretty.quote o prt_term) ts));
+    fun prt_asm (b, ts) =
+      Pretty.block (Pretty.breaks
+        ((if Binding.is_empty b then [] else [Binding.pretty b, Pretty.str ":"]) @
+          map (Pretty.quote o prt_term) ts));
 
     fun prt_sect _ _ _ [] = []
       | prt_sect head sep prt xs =