--- a/src/Pure/Syntax/mixfix.ML Wed Mar 30 14:59:12 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML Wed Mar 30 15:15:12 2016 +0200
@@ -9,7 +9,6 @@
datatype mixfix =
NoSyn |
Mixfix of Input.source * int list * int * Position.range |
- Delimfix of Input.source * Position.range |
Infix of Input.source * int * Position.range |
Infixl of Input.source * int * Position.range |
Infixr of Input.source * int * Position.range |
@@ -20,6 +19,7 @@
signature MIXFIX =
sig
include BASIC_MIXFIX
+ val mixfix: string -> mixfix
val is_empty: mixfix -> bool
val equal: mixfix * mixfix -> bool
val range_of: mixfix -> Position.range
@@ -42,20 +42,20 @@
datatype mixfix =
NoSyn |
Mixfix of Input.source * int list * int * Position.range |
- Delimfix of Input.source * Position.range |
Infix of Input.source * int * Position.range |
Infixl of Input.source * int * Position.range |
Infixr of Input.source * int * Position.range |
Binder of Input.source * int * int * Position.range |
Structure of Position.range;
+fun mixfix s = Mixfix (Input.string s, [], 1000, Position.no_range);
+
fun is_empty NoSyn = true
| is_empty _ = false;
fun equal (NoSyn, NoSyn) = true
| equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) =
Input.equal_content (sy, sy') andalso ps = ps' andalso p = p'
- | equal (Delimfix (sy, _), Delimfix (sy', _)) = Input.equal_content (sy, sy')
| equal (Infix (sy, p, _), Infix (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
| equal (Infixl (sy, p, _), Infixl (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
| equal (Infixr (sy, p, _), Infixr (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
@@ -66,7 +66,6 @@
fun range_of NoSyn = Position.no_range
| range_of (Mixfix (_, _, _, range)) = range
- | range_of (Delimfix (_, range)) = range
| range_of (Infix (_, _, range)) = range
| range_of (Infixl (_, _, range)) = range
| range_of (Infixr (_, _, range)) = range
@@ -77,7 +76,6 @@
fun reset_pos NoSyn = NoSyn
| reset_pos (Mixfix (sy, ps, p, _)) = Mixfix (Input.reset_pos sy, ps, p, Position.no_range)
- | reset_pos (Delimfix (sy, _)) = Delimfix (Input.reset_pos sy, Position.no_range)
| reset_pos (Infix (sy, p, _)) = Infix (Input.reset_pos sy, p, Position.no_range)
| reset_pos (Infixl (sy, p, _)) = Infixl (Input.reset_pos sy, p, Position.no_range)
| reset_pos (Infixr (sy, p, _)) = Infixr (Input.reset_pos sy, p, Position.no_range)
@@ -100,7 +98,6 @@
fun pretty_mixfix NoSyn = Pretty.str ""
| pretty_mixfix (Mixfix (s, ps, p, _)) =
parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
- | pretty_mixfix (Delimfix (s, _)) = parens [quoted s]
| pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
| pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
| pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
@@ -115,7 +112,6 @@
fun mixfix_args NoSyn = 0
| mixfix_args (Mixfix (sy, _, _, _)) = Syntax_Ext.mixfix_args sy
- | mixfix_args (Delimfix (sy, _)) = Syntax_Ext.mixfix_args sy
| mixfix_args (Infix (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
| mixfix_args (Infixl (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
| mixfix_args (Infixr (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
@@ -141,8 +137,6 @@
fun mfix_of (_, _, NoSyn) = NONE
| mfix_of (t, ty, Mixfix (sy, ps, p, range)) =
SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p, Position.set_range range))
- | mfix_of (t, ty, Delimfix (sy, range)) =
- SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000, Position.set_range range))
| mfix_of (t, ty, Infix (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p range)
| mfix_of (t, ty, Infixl (sy, p, range)) = SOME (mk_infix sy ty t p (p + 1) p range)
| mfix_of (t, ty, Infixr (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) p p range)
@@ -183,8 +177,6 @@
fun mfix_of (_, _, NoSyn) = []
| mfix_of (c, ty, Mixfix (sy, ps, p, range)) =
[Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, Position.set_range range)]
- | mfix_of (c, ty, Delimfix (sy, range)) =
- [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000, Position.set_range range)]
| mfix_of (c, ty, Infix (sy, p, range)) = mk_infix sy ty c (p + 1) (p + 1) p range
| mfix_of (c, ty, Infixl (sy, p, range)) = mk_infix sy ty c p (p + 1) p range
| mfix_of (c, ty, Infixr (sy, p, range)) = mk_infix sy ty c (p + 1) p p range