pretty-print according to defaults of input syntax;
authorwenzelm
Fri May 25 21:01:51 2018 +0200 (21 months ago)
changeset 6827353788963c4dc
parent 68272 ddeb6847451a
child 68274 867bd42b3f59
pretty-print according to defaults of input syntax;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri May 25 21:00:47 2018 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri May 25 21:01:51 2018 +0200
     1.3 @@ -97,12 +97,18 @@
     1.4  
     1.5  fun pretty_mixfix NoSyn = Pretty.str ""
     1.6    | pretty_mixfix (Mixfix (s, ps, p, _)) =
     1.7 -      parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
     1.8 +      parens
     1.9 +        (Pretty.breaks
    1.10 +          (quoted s ::
    1.11 +            (if null ps then [] else [brackets (Pretty.commas (map int ps))]) @
    1.12 +            (if p = 1000 then [] else [int p])))
    1.13    | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
    1.14    | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    1.15    | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixr", quoted s, int p])
    1.16    | pretty_mixfix (Binder (s, p1, p2, _)) =
    1.17 -      parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2])
    1.18 +      parens
    1.19 +        (Pretty.breaks
    1.20 +          ([keyword "binder", quoted s] @ (if p1 = p2 then [] else [brackets [int p1]]) @ [int p2]))
    1.21    | pretty_mixfix (Structure _) = parens [keyword "structure"];
    1.22  
    1.23  end;