tuned;
authorwenzelm
Wed Mar 30 14:59:12 2016 +0200 (2016-03-30)
changeset 62760aabcc727aa2d
parent 62759 d16b2ec535ba
child 62761 5c672b22dcc2
tuned;
src/Pure/Isar/parse.ML
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Isar/parse.ML	Wed Mar 30 14:52:23 2016 +0200
     1.2 +++ b/src/Pure/Isar/parse.ML	Wed Mar 30 14:59:12 2016 +0200
     1.3 @@ -320,29 +320,29 @@
     1.4  val mfix =
     1.5    input string --
     1.6      !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat 1000)
     1.7 -  >> (fn (sy, (ps, p)) => Mixfix (sy, ps, p, Position.no_range));
     1.8 +  >> (fn (sy, (ps, p)) => fn range => Mixfix (sy, ps, p, range));
     1.9  
    1.10  val infx =
    1.11 -  $$$ "infix" |-- !!! (input string -- nat >> (fn (sy, p) => Infix (sy, p, Position.no_range)));
    1.12 +  $$$ "infix" |-- !!! (input string -- nat >> (fn (sy, p) => fn range => Infix (sy, p, range)));
    1.13  
    1.14  val infxl =
    1.15 -  $$$ "infixl" |-- !!! (input string -- nat >> (fn (sy, p) => Infixl (sy, p, Position.no_range)));
    1.16 +  $$$ "infixl" |-- !!! (input string -- nat >> (fn (sy, p) => fn range => Infixl (sy, p, range)));
    1.17  
    1.18  val infxr =
    1.19 -  $$$ "infixr" |-- !!! (input string -- nat >> (fn (sy, p) => Infixr (sy, p, Position.no_range)));
    1.20 +  $$$ "infixr" |-- !!! (input string -- nat >> (fn (sy, p) => fn range => Infixr (sy, p, range)));
    1.21  
    1.22 -val strcture = $$$ "structure" >> K (Structure Position.no_range);
    1.23 +val strcture = $$$ "structure" >> K Structure;
    1.24  
    1.25  val binder =
    1.26    $$$ "binder" |--
    1.27      !!! (input string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
    1.28 -  >> (fn (sy, (p, q)) => Binder (sy, p, q, Position.no_range));
    1.29 +  >> (fn (sy, (p, q)) => fn range => Binder (sy, p, q, range));
    1.30  
    1.31  val mixfix_body = mfix || strcture || binder || infxl || infxr || infx;
    1.32  
    1.33  fun annotation guard body =
    1.34    Scan.trace ($$$ "(" |-- guard (body --| $$$ ")"))
    1.35 -    >> (fn (mx, toks) => Mixfix.set_range (Token.range_of toks) mx);
    1.36 +    >> (fn (mx, toks) => mx (Token.range_of toks));
    1.37  
    1.38  fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn;
    1.39  
     2.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Mar 30 14:52:23 2016 +0200
     2.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Mar 30 14:59:12 2016 +0200
     2.3 @@ -22,7 +22,6 @@
     2.4    include BASIC_MIXFIX
     2.5    val is_empty: mixfix -> bool
     2.6    val equal: mixfix * mixfix -> bool
     2.7 -  val set_range: Position.range -> mixfix -> mixfix
     2.8    val range_of: mixfix -> Position.range
     2.9    val pos_of: mixfix -> Position.T
    2.10    val reset_pos: mixfix -> mixfix
    2.11 @@ -65,17 +64,6 @@
    2.12    | equal (Structure _, Structure _) = true
    2.13    | equal _ = false;
    2.14  
    2.15 -fun set_range range mx =
    2.16 -  (case mx of
    2.17 -    NoSyn => NoSyn
    2.18 -  | Mixfix (sy, ps, p, _) => Mixfix (sy, ps, p, range)
    2.19 -  | Delimfix (sy, _) => Delimfix (sy, range)
    2.20 -  | Infix (sy, p, _) => Infix (sy, p, range)
    2.21 -  | Infixl (sy, p, _) => Infixl (sy, p, range)
    2.22 -  | Infixr (sy, p, _) => Infixr (sy, p, range)
    2.23 -  | Binder (sy, p, q, _) => Binder (sy, p, q, range)
    2.24 -  | Structure _ => Structure range);
    2.25 -
    2.26  fun range_of NoSyn = Position.no_range
    2.27    | range_of (Mixfix (_, _, _, range)) = range
    2.28    | range_of (Delimfix (_, range)) = range