equal
deleted
inserted
replaced
23 sig |
23 sig |
24 include MIXFIX0 |
24 include MIXFIX0 |
25 val no_syn: 'a * 'b -> 'a * 'b * mixfix |
25 val no_syn: 'a * 'b -> 'a * 'b * mixfix |
26 val type_name: string -> mixfix -> string |
26 val type_name: string -> mixfix -> string |
27 val const_name: string -> mixfix -> string |
27 val const_name: string -> mixfix -> string |
|
28 val fix_mixfix: string -> mixfix -> mixfix |
28 val mixfix_args: mixfix -> int |
29 val mixfix_args: mixfix -> int |
29 val pure_nonterms: string list |
30 val pure_nonterms: string list |
30 val pure_syntax: (string * string * mixfix) list |
31 val pure_syntax: (string * string * mixfix) list |
31 val pure_appl_syntax: (string * string * mixfix) list |
32 val pure_appl_syntax: (string * string * mixfix) list |
32 val pure_applC_syntax: (string * string * mixfix) list |
33 val pure_applC_syntax: (string * string * mixfix) list |
82 fun const_name c (InfixlName _) = c |
83 fun const_name c (InfixlName _) = c |
83 | const_name c (InfixrName _) = c |
84 | const_name c (InfixrName _) = c |
84 | const_name c (Infixl _) = "op " ^ strip_esc c |
85 | const_name c (Infixl _) = "op " ^ strip_esc c |
85 | const_name c (Infixr _) = "op " ^ strip_esc c |
86 | const_name c (Infixr _) = "op " ^ strip_esc c |
86 | const_name c _ = c; |
87 | const_name c _ = c; |
|
88 |
|
89 fun fix_mixfix c (Infixl p) = (InfixlName (c, p)) |
|
90 | fix_mixfix c (Infixr p) = (InfixrName (c, p)) |
|
91 | fix_mixfix _ mx = mx; |
87 |
92 |
88 |
93 |
89 (* mixfix_args *) |
94 (* mixfix_args *) |
90 |
95 |
91 fun mixfix_args NoSyn = 0 |
96 fun mixfix_args NoSyn = 0 |