tuned output;
authorwenzelm
Sun May 03 17:36:46 2015 +0200 (2015-05-03)
changeset 602435901cb4db0ae
parent 60242 3a8501876dba
child 60244 523ec7e4b022
tuned output;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun May 03 17:19:27 2015 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun May 03 17:36:46 2015 +0200
     1.3 @@ -160,11 +160,13 @@
     1.4    | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)];
     1.5  
     1.6  fun pretty_binding ctxt (b, atts) sep =
     1.7 -  if is_empty_binding (b, atts) then []
     1.8 -  else if Binding.is_empty b then
     1.9 -    [Pretty.block (pretty_attribs ctxt atts @ [Pretty.str sep])]
    1.10 -  else
    1.11 -    [Pretty.block (Binding.pretty b :: Pretty.brk 1 :: pretty_attribs ctxt atts @ [Pretty.str sep])];
    1.12 +  (case (Binding.is_empty b, null atts) of
    1.13 +    (true, true) => []
    1.14 +  | (false, true) => [Pretty.block [Binding.pretty b, Pretty.str sep]]
    1.15 +  | (true, false) => [Pretty.block (pretty_attribs ctxt atts @ [Pretty.str sep])]
    1.16 +  | (false, false) =>
    1.17 +      [Pretty.block
    1.18 +        (Binding.pretty b :: Pretty.brk 1 :: pretty_attribs ctxt atts @ [Pretty.str sep])]);
    1.19  
    1.20  
    1.21  (* get attributes *)