src/Pure/Syntax/mixfix.ML
changeset 62761 5c672b22dcc2
parent 62760 aabcc727aa2d
child 62766 70b73465f636
--- 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