tuned output -- avoid empty quites and extra breaks;
authorwenzelm
Sun May 03 17:19:27 2015 +0200 (2015-05-03)
changeset 602423a8501876dba
parent 60241 cde717a55db7
child 60243 5901cb4db0ae
tuned output -- avoid empty quites and extra breaks;
src/Pure/Isar/attrib.ML
src/Pure/Isar/element.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun May 03 16:45:07 2015 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun May 03 17:19:27 2015 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    val check_name: Proof.context -> xstring * Position.T -> string
     1.5    val check_src: Proof.context -> Token.src -> Token.src
     1.6    val pretty_attribs: Proof.context -> Token.src list -> Pretty.T list
     1.7 +  val pretty_binding: Proof.context -> binding -> string -> Pretty.T list
     1.8    val attribute: Proof.context -> Token.src -> attribute
     1.9    val attribute_global: theory -> Token.src -> attribute
    1.10    val attribute_cmd: Proof.context -> Token.src -> attribute
    1.11 @@ -158,6 +159,13 @@
    1.12  fun pretty_attribs _ [] = []
    1.13    | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)];
    1.14  
    1.15 +fun pretty_binding ctxt (b, atts) sep =
    1.16 +  if is_empty_binding (b, atts) then []
    1.17 +  else if Binding.is_empty b then
    1.18 +    [Pretty.block (pretty_attribs ctxt atts @ [Pretty.str sep])]
    1.19 +  else
    1.20 +    [Pretty.block (Binding.pretty b :: Pretty.brk 1 :: pretty_attribs ctxt atts @ [Pretty.str sep])];
    1.21 +
    1.22  
    1.23  (* get attributes *)
    1.24  
     2.1 --- a/src/Pure/Isar/element.ML	Sun May 03 16:45:07 2015 +0200
     2.2 +++ b/src/Pure/Isar/element.ML	Sun May 03 17:19:27 2015 +0200
     2.3 @@ -112,12 +112,6 @@
     2.4        Pretty.block [Pretty.keyword2 keyword, Pretty.brk 1, x] ::
     2.5          map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword2 sep, Pretty.brk 1, y]) ys;
     2.6  
     2.7 -fun pretty_name_atts ctxt (b, atts) sep =
     2.8 -  if Attrib.is_empty_binding (b, atts) then []
     2.9 -  else
    2.10 -    [Pretty.block (Pretty.breaks
    2.11 -      (Binding.pretty b :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
    2.12 -
    2.13  
    2.14  (* pretty_stmt *)
    2.15  
    2.16 @@ -126,10 +120,10 @@
    2.17      val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
    2.18      val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
    2.19      val prt_terms = separate (Pretty.keyword2 "and") o map prt_term;
    2.20 -    val prt_name_atts = pretty_name_atts ctxt;
    2.21 +    val prt_binding = Attrib.pretty_binding ctxt;
    2.22  
    2.23      fun prt_show (a, ts) =
    2.24 -      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
    2.25 +      Pretty.block (Pretty.breaks (prt_binding a ":" @ prt_terms (map fst ts)));
    2.26  
    2.27      fun prt_var (x, SOME T) = Pretty.block
    2.28            [Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
    2.29 @@ -153,10 +147,8 @@
    2.30      val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
    2.31      val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    2.32  
    2.33 -    fun prt_name_atts (b, atts) sep =
    2.34 -      if not show_attribs orelse null atts then
    2.35 -        [Pretty.block [Binding.pretty b, Pretty.str sep]]
    2.36 -      else pretty_name_atts ctxt (b, atts) sep;
    2.37 +    fun prt_binding (b, atts) =
    2.38 +      Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
    2.39  
    2.40      fun prt_fact (ths, atts) =
    2.41        if not show_attribs orelse null atts then map prt_thm ths
    2.42 @@ -174,12 +166,12 @@
    2.43      fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
    2.44  
    2.45      fun prt_asm (a, ts) =
    2.46 -      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
    2.47 +      Pretty.block (Pretty.breaks (prt_binding a ":" @ map (prt_term o fst) ts));
    2.48      fun prt_def (a, (t, _)) =
    2.49 -      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ [prt_term t]));
    2.50 +      Pretty.block (Pretty.breaks (prt_binding a ":" @ [prt_term t]));
    2.51  
    2.52      fun prt_note (a, ths) =
    2.53 -      Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths)));
    2.54 +      Pretty.block (Pretty.breaks (flat (prt_binding a " =" :: map prt_fact ths)));
    2.55    in
    2.56      fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes)
    2.57       | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs)
     3.1 --- a/src/Pure/Isar/proof_context.ML	Sun May 03 16:45:07 2015 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Sun May 03 17:19:27 2015 +0200
     3.3 @@ -1346,9 +1346,10 @@
     3.4        [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1,
     3.5          Pretty.quote (prt_term t)];
     3.6  
     3.7 -    fun prt_asm (b, ts) = Pretty.block (Pretty.breaks
     3.8 -      ((if Binding.is_empty b then []
     3.9 -        else [Binding.pretty b, Pretty.str ":"]) @ map (Pretty.quote o prt_term) ts));
    3.10 +    fun prt_asm (b, ts) =
    3.11 +      Pretty.block (Pretty.breaks
    3.12 +        ((if Binding.is_empty b then [] else [Binding.pretty b, Pretty.str ":"]) @
    3.13 +          map (Pretty.quote o prt_term) ts));
    3.14  
    3.15      fun prt_sect _ _ _ [] = []
    3.16        | prt_sect head sep prt xs =