# HG changeset patch # User wenzelm # Date 1527274911 -7200 # Node ID 53788963c4dccf3a0e3cfad7c5fa0b3eae178390 # Parent ddeb6847451a06476f217edaf8d8c46c1a4ec54a pretty-print according to defaults of input syntax; diff -r ddeb6847451a -r 53788963c4dc src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Fri May 25 21:00:47 2018 +0200 +++ b/src/Pure/Syntax/mixfix.ML Fri May 25 21:01:51 2018 +0200 @@ -97,12 +97,18 @@ fun pretty_mixfix NoSyn = Pretty.str "" | pretty_mixfix (Mixfix (s, ps, p, _)) = - parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p]) + parens + (Pretty.breaks + (quoted s :: + (if null ps then [] else [brackets (Pretty.commas (map int ps))]) @ + (if p = 1000 then [] else [int p]))) | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p]) | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixr", quoted s, int p]) | pretty_mixfix (Binder (s, p1, p2, _)) = - parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2]) + parens + (Pretty.breaks + ([keyword "binder", quoted s] @ (if p1 = p2 then [] else [brackets [int p1]]) @ [int p2])) | pretty_mixfix (Structure _) = parens [keyword "structure"]; end;