23 val is_empty: mixfix -> bool |
23 val is_empty: mixfix -> bool |
24 val equal: mixfix * mixfix -> bool |
24 val equal: mixfix * mixfix -> bool |
25 val set_range: Position.range -> mixfix -> mixfix |
25 val set_range: Position.range -> mixfix -> mixfix |
26 val range_of: mixfix -> Position.range |
26 val range_of: mixfix -> Position.range |
27 val pos_of: mixfix -> Position.T |
27 val pos_of: mixfix -> Position.T |
|
28 val reset_pos: mixfix -> mixfix |
28 val pretty_mixfix: mixfix -> Pretty.T |
29 val pretty_mixfix: mixfix -> Pretty.T |
29 val mixfix_args: mixfix -> int |
30 val mixfix_args: mixfix -> int |
30 val mixfixT: mixfix -> typ |
31 val mixfixT: mixfix -> typ |
31 val make_type: int -> typ |
32 val make_type: int -> typ |
32 val binder_name: string -> string |
33 val binder_name: string -> string |
83 | range_of (Infixr (_, _, range)) = range |
84 | range_of (Infixr (_, _, range)) = range |
84 | range_of (Binder (_, _, _, range)) = range |
85 | range_of (Binder (_, _, _, range)) = range |
85 | range_of (Structure range) = range; |
86 | range_of (Structure range) = range; |
86 |
87 |
87 val pos_of = Position.set_range o range_of; |
88 val pos_of = Position.set_range o range_of; |
|
89 |
|
90 fun reset_pos NoSyn = NoSyn |
|
91 | reset_pos (Mixfix (sy, ps, p, _)) = Mixfix (Input.reset_pos sy, ps, p, Position.no_range) |
|
92 | reset_pos (Delimfix (sy, _)) = Delimfix (Input.reset_pos sy, Position.no_range) |
|
93 | reset_pos (Infix (sy, p, _)) = Infix (Input.reset_pos sy, p, Position.no_range) |
|
94 | reset_pos (Infixl (sy, p, _)) = Infixl (Input.reset_pos sy, p, Position.no_range) |
|
95 | reset_pos (Infixr (sy, p, _)) = Infixr (Input.reset_pos sy, p, Position.no_range) |
|
96 | reset_pos (Binder (sy, p, q, _)) = Binder (Input.reset_pos sy, p, q, Position.no_range) |
|
97 | reset_pos (Structure _) = Structure Position.no_range; |
88 |
98 |
89 |
99 |
90 (* pretty_mixfix *) |
100 (* pretty_mixfix *) |
91 |
101 |
92 local |
102 local |