24 signature MIXFIX1 = |
24 signature MIXFIX1 = |
25 sig |
25 sig |
26 include MIXFIX0 |
26 include MIXFIX0 |
27 val literal: string -> mixfix |
27 val literal: string -> mixfix |
28 val no_syn: 'a * 'b -> 'a * 'b * mixfix |
28 val no_syn: 'a * 'b -> 'a * 'b * mixfix |
29 val string_of_mixfix: mixfix -> string |
29 val pretty_mixfix: mixfix -> Pretty.T |
30 val type_name: string -> mixfix -> string |
30 val type_name: string -> mixfix -> string |
31 val const_name: string -> mixfix -> string |
31 val const_name: string -> mixfix -> string |
32 val fix_mixfix: string -> mixfix -> mixfix |
32 val fix_mixfix: string -> mixfix -> mixfix |
33 val unlocalize_mixfix: mixfix -> mixfix |
33 val unlocalize_mixfix: mixfix -> mixfix |
34 val mixfix_args: mixfix -> int |
34 val mixfix_args: mixfix -> int |
64 val literal = Delimfix o SynExt.escape_mfix; |
64 val literal = Delimfix o SynExt.escape_mfix; |
65 |
65 |
66 fun no_syn (x, y) = (x, y, NoSyn); |
66 fun no_syn (x, y) = (x, y, NoSyn); |
67 |
67 |
68 |
68 |
69 (* string_of_mixfix *) |
69 (* pretty_mixfix *) |
70 |
70 |
71 val parens = enclose "(" ")"; |
71 local |
72 val brackets = enclose "[" "]"; |
72 |
73 val spaces = space_implode " "; |
73 val quoted = Pretty.quote o Pretty.str; |
74 |
74 val keyword = Pretty.keyword; |
75 fun string_of_mixfix NoSyn = "" |
75 val parens = Pretty.enclose "(" ")"; |
76 | string_of_mixfix (Mixfix (sy, ps, p)) = |
76 val brackets = Pretty.enclose "[" "]"; |
77 parens (spaces [quote sy, brackets (commas (map string_of_int ps)), string_of_int p]) |
77 val int = Pretty.str o string_of_int; |
78 | string_of_mixfix (Delimfix sy) = parens (quote sy) |
78 |
79 | string_of_mixfix (InfixName (sy, p)) = parens (spaces ["infix", quote sy, string_of_int p]) |
79 in |
80 | string_of_mixfix (InfixlName (sy, p)) = parens (spaces ["infixl", quote sy, string_of_int p]) |
80 |
81 | string_of_mixfix (InfixrName (sy, p)) = parens (spaces ["infixl", quote sy, string_of_int p]) |
81 fun pretty_mixfix NoSyn = Pretty.str "" |
82 | string_of_mixfix (Infix p) = parens (spaces ["infix", string_of_int p]) |
82 | pretty_mixfix (Mixfix (s, ps, p)) = |
83 | string_of_mixfix (Infixl p) = parens (spaces ["infixl", string_of_int p]) |
83 parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p]) |
84 | string_of_mixfix (Infixr p) = parens (spaces ["infixr", string_of_int p]) |
84 | pretty_mixfix (Delimfix s) = parens [quoted s] |
85 | string_of_mixfix (Binder (sy, p1, p2)) = |
85 | pretty_mixfix (InfixName (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p]) |
86 parens (spaces ["binder", quote sy, brackets (string_of_int p1), string_of_int p2]) |
86 | pretty_mixfix (InfixlName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) |
87 | string_of_mixfix Structure = "(structure)"; |
87 | pretty_mixfix (InfixrName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) |
|
88 | pretty_mixfix (Infix p) = parens (Pretty.breaks [keyword "infix", int p]) |
|
89 | pretty_mixfix (Infixl p) = parens (Pretty.breaks [keyword "infixl", int p]) |
|
90 | pretty_mixfix (Infixr p) = parens (Pretty.breaks [keyword "infixr", int p]) |
|
91 | pretty_mixfix (Binder (s, p1, p2)) = |
|
92 parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2]) |
|
93 | pretty_mixfix Structure = parens [keyword "structure"]; |
|
94 |
|
95 end; |
88 |
96 |
89 |
97 |
90 (* syntax specifications *) |
98 (* syntax specifications *) |
91 |
99 |
92 fun strip ("'" :: c :: cs) = c :: strip cs |
100 fun strip ("'" :: c :: cs) = c :: strip cs |