src/Pure/Syntax/mixfix.ML
changeset 68271 77f6fa78b6e1
parent 67398 5eb932e604a2
child 68273 53788963c4dc
equal deleted inserted replaced
68269:5ff0ccc74884 68271:77f6fa78b6e1
    98 fun pretty_mixfix NoSyn = Pretty.str ""
    98 fun pretty_mixfix NoSyn = Pretty.str ""
    99   | pretty_mixfix (Mixfix (s, ps, p, _)) =
    99   | pretty_mixfix (Mixfix (s, ps, p, _)) =
   100       parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
   100       parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
   101   | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
   101   | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
   102   | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
   102   | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
   103   | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
   103   | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixr", quoted s, int p])
   104   | pretty_mixfix (Binder (s, p1, p2, _)) =
   104   | pretty_mixfix (Binder (s, p1, p2, _)) =
   105       parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2])
   105       parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2])
   106   | pretty_mixfix (Structure _) = parens [keyword "structure"];
   106   | pretty_mixfix (Structure _) = parens [keyword "structure"];
   107 
   107 
   108 end;
   108 end;