85 |
85 |
86 (* pretty_mixfix *) |
86 (* pretty_mixfix *) |
87 |
87 |
88 local |
88 local |
89 |
89 |
90 val quoted = Pretty.quote o Pretty.str o #1 o Input.source_content; |
90 val template = Pretty.quote o Pretty.str o #1 o Input.source_content; |
91 val keyword = Pretty.keyword2; |
91 val keyword = Pretty.keyword2; |
92 val parens = Pretty.enclose "(" ")"; |
92 val parens = Pretty.enclose "(" ")"; |
93 val brackets = Pretty.enclose "[" "]"; |
93 val brackets = Pretty.enclose "[" "]"; |
94 val int = Pretty.str o string_of_int; |
94 val int = Pretty.str o string_of_int; |
95 |
95 |
97 |
97 |
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 |
100 parens |
101 (Pretty.breaks |
101 (Pretty.breaks |
102 (quoted s :: |
102 (template s :: |
103 (if null ps then [] else [brackets (Pretty.commas (map int ps))]) @ |
103 (if null ps then [] else [brackets (Pretty.commas (map int ps))]) @ |
104 (if p = 1000 then [] else [int p]))) |
104 (if p = 1000 then [] else [int p]))) |
105 | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p]) |
105 | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", template s, int p]) |
106 | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) |
106 | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", template s, int p]) |
107 | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixr", quoted s, int p]) |
107 | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixr", template s, int p]) |
108 | pretty_mixfix (Binder (s, p1, p2, _)) = |
108 | pretty_mixfix (Binder (s, p1, p2, _)) = |
109 parens |
109 parens |
110 (Pretty.breaks |
110 (Pretty.breaks |
111 ([keyword "binder", quoted s] @ (if p1 = p2 then [] else [brackets [int p1]]) @ [int p2])) |
111 ([keyword "binder", template s] @ |
|
112 (if p1 = p2 then [] else [brackets [int p1]]) @ [int p2])) |
112 | pretty_mixfix (Structure _) = parens [keyword "structure"]; |
113 | pretty_mixfix (Structure _) = parens [keyword "structure"]; |
113 |
114 |
114 end; |
115 end; |
115 |
116 |
116 |
117 |