19 signature MIXFIX = |
19 signature MIXFIX = |
20 sig |
20 sig |
21 include BASIC_MIXFIX |
21 include BASIC_MIXFIX |
22 val mixfix: string -> mixfix |
22 val mixfix: string -> mixfix |
23 val is_empty: mixfix -> bool |
23 val is_empty: mixfix -> bool |
|
24 val is_infix: mixfix -> bool |
24 val equal: mixfix * mixfix -> bool |
25 val equal: mixfix * mixfix -> bool |
25 val range_of: mixfix -> Position.range |
26 val range_of: mixfix -> Position.range |
26 val pos_of: mixfix -> Position.T |
27 val pos_of: mixfix -> Position.T |
27 val reset_pos: mixfix -> mixfix |
28 val reset_pos: mixfix -> mixfix |
28 val pretty_mixfix: mixfix -> Pretty.T |
29 val pretty_mixfix: mixfix -> Pretty.T |
51 |
52 |
52 fun mixfix s = Mixfix (Input.string s, [], 1000, Position.no_range); |
53 fun mixfix s = Mixfix (Input.string s, [], 1000, Position.no_range); |
53 |
54 |
54 fun is_empty NoSyn = true |
55 fun is_empty NoSyn = true |
55 | is_empty _ = false; |
56 | is_empty _ = false; |
|
57 |
|
58 fun is_infix (Infix _) = true |
|
59 | is_infix (Infixl _) = true |
|
60 | is_infix (Infixr _) = true |
|
61 | is_infix _ = false; |
56 |
62 |
57 fun equal (NoSyn, NoSyn) = true |
63 fun equal (NoSyn, NoSyn) = true |
58 | equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) = |
64 | equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) = |
59 Input.equal_content (sy, sy') andalso ps = ps' andalso p = p' |
65 Input.equal_content (sy, sy') andalso ps = ps' andalso p = p' |
60 | equal (Infix (sy, p, _), Infix (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p' |
66 | equal (Infix (sy, p, _), Infix (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p' |