src/Pure/Syntax/mixfix.ML
changeset 62761 5c672b22dcc2
parent 62760 aabcc727aa2d
child 62766 70b73465f636
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Mar 30 14:59:12 2016 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Mar 30 15:15:12 2016 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4    datatype mixfix =
     1.5      NoSyn |
     1.6      Mixfix of Input.source * int list * int * Position.range |
     1.7 -    Delimfix of Input.source * Position.range |
     1.8      Infix of Input.source * int * Position.range |
     1.9      Infixl of Input.source * int * Position.range |
    1.10      Infixr of Input.source * int * Position.range |
    1.11 @@ -20,6 +19,7 @@
    1.12  signature MIXFIX =
    1.13  sig
    1.14    include BASIC_MIXFIX
    1.15 +  val mixfix: string -> mixfix
    1.16    val is_empty: mixfix -> bool
    1.17    val equal: mixfix * mixfix -> bool
    1.18    val range_of: mixfix -> Position.range
    1.19 @@ -42,20 +42,20 @@
    1.20  datatype mixfix =
    1.21    NoSyn |
    1.22    Mixfix of Input.source * int list * int * Position.range |
    1.23 -  Delimfix of Input.source * Position.range |
    1.24    Infix of Input.source * int * Position.range |
    1.25    Infixl of Input.source * int * Position.range |
    1.26    Infixr of Input.source * int * Position.range |
    1.27    Binder of Input.source * int * int * Position.range |
    1.28    Structure of Position.range;
    1.29  
    1.30 +fun mixfix s = Mixfix (Input.string s, [], 1000, Position.no_range);
    1.31 +
    1.32  fun is_empty NoSyn = true
    1.33    | is_empty _ = false;
    1.34  
    1.35  fun equal (NoSyn, NoSyn) = true
    1.36    | equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) =
    1.37        Input.equal_content (sy, sy') andalso ps = ps' andalso p = p'
    1.38 -  | equal (Delimfix (sy, _), Delimfix (sy', _)) = Input.equal_content (sy, sy')
    1.39    | equal (Infix (sy, p, _), Infix (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
    1.40    | equal (Infixl (sy, p, _), Infixl (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
    1.41    | equal (Infixr (sy, p, _), Infixr (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
    1.42 @@ -66,7 +66,6 @@
    1.43  
    1.44  fun range_of NoSyn = Position.no_range
    1.45    | range_of (Mixfix (_, _, _, range)) = range
    1.46 -  | range_of (Delimfix (_, range)) = range
    1.47    | range_of (Infix (_, _, range)) = range
    1.48    | range_of (Infixl (_, _, range)) = range
    1.49    | range_of (Infixr (_, _, range)) = range
    1.50 @@ -77,7 +76,6 @@
    1.51  
    1.52  fun reset_pos NoSyn = NoSyn
    1.53    | reset_pos (Mixfix (sy, ps, p, _)) = Mixfix (Input.reset_pos sy, ps, p, Position.no_range)
    1.54 -  | reset_pos (Delimfix (sy, _)) = Delimfix (Input.reset_pos sy, Position.no_range)
    1.55    | reset_pos (Infix (sy, p, _)) = Infix (Input.reset_pos sy, p, Position.no_range)
    1.56    | reset_pos (Infixl (sy, p, _)) = Infixl (Input.reset_pos sy, p, Position.no_range)
    1.57    | reset_pos (Infixr (sy, p, _)) = Infixr (Input.reset_pos sy, p, Position.no_range)
    1.58 @@ -100,7 +98,6 @@
    1.59  fun pretty_mixfix NoSyn = Pretty.str ""
    1.60    | pretty_mixfix (Mixfix (s, ps, p, _)) =
    1.61        parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
    1.62 -  | pretty_mixfix (Delimfix (s, _)) = parens [quoted s]
    1.63    | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
    1.64    | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    1.65    | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    1.66 @@ -115,7 +112,6 @@
    1.67  
    1.68  fun mixfix_args NoSyn = 0
    1.69    | mixfix_args (Mixfix (sy, _, _, _)) = Syntax_Ext.mixfix_args sy
    1.70 -  | mixfix_args (Delimfix (sy, _)) = Syntax_Ext.mixfix_args sy
    1.71    | mixfix_args (Infix (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
    1.72    | mixfix_args (Infixl (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
    1.73    | mixfix_args (Infixr (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
    1.74 @@ -141,8 +137,6 @@
    1.75      fun mfix_of (_, _, NoSyn) = NONE
    1.76        | mfix_of (t, ty, Mixfix (sy, ps, p, range)) =
    1.77            SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p, Position.set_range range))
    1.78 -      | mfix_of (t, ty, Delimfix (sy, range)) =
    1.79 -          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000, Position.set_range range))
    1.80        | mfix_of (t, ty, Infix (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p range)
    1.81        | mfix_of (t, ty, Infixl (sy, p, range)) = SOME (mk_infix sy ty t p (p + 1) p range)
    1.82        | mfix_of (t, ty, Infixr (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) p p range)
    1.83 @@ -183,8 +177,6 @@
    1.84      fun mfix_of (_, _, NoSyn) = []
    1.85        | mfix_of (c, ty, Mixfix (sy, ps, p, range)) =
    1.86            [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, Position.set_range range)]
    1.87 -      | mfix_of (c, ty, Delimfix (sy, range)) =
    1.88 -          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000, Position.set_range range)]
    1.89        | mfix_of (c, ty, Infix (sy, p, range)) = mk_infix sy ty c (p + 1) (p + 1) p range
    1.90        | mfix_of (c, ty, Infixl (sy, p, range)) = mk_infix sy ty c p (p + 1) p range
    1.91        | mfix_of (c, ty, Infixr (sy, p, range)) = mk_infix sy ty c (p + 1) p p range