src/Pure/Isar/token.ML
changeset 62797 e08c44eed27f
parent 62782 057e8dbe4326
child 62799 46e6f91c4da1
     1.1 --- a/src/Pure/Isar/token.ML	Fri Apr 01 17:23:15 2016 +0200
     1.2 +++ b/src/Pure/Isar/token.ML	Fri Apr 01 17:37:46 2016 +0200
     1.3 @@ -183,13 +183,13 @@
     1.4  fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
     1.5  fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
     1.6  
     1.7 -fun reset_pos pos (Token ((x, _), y, z)) =
     1.8 +fun reset_range pos (Token ((x, _), y, z)) =
     1.9    let val pos' = Position.reset_range pos
    1.10    in Token ((x, (pos', pos')), y, z) end;
    1.11  
    1.12  fun range_of (toks as tok :: _) =
    1.13        let val pos' = end_pos_of (List.last toks)
    1.14 -      in Position.range (pos_of tok) pos' end
    1.15 +      in Position.range (pos_of tok, pos') end
    1.16    | range_of [] = Position.no_range;
    1.17  
    1.18  
    1.19 @@ -666,7 +666,7 @@
    1.20  fun make ((k, n), s) pos =
    1.21    let
    1.22      val pos' = Position.advance_offset n pos;
    1.23 -    val range = Position.range pos pos';
    1.24 +    val range = Position.range (pos, pos');
    1.25      val tok =
    1.26        if 0 <= k andalso k < Vector.length immediate_kinds then
    1.27          Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot)
    1.28 @@ -678,7 +678,7 @@
    1.29  
    1.30  fun make_string (s, pos) =
    1.31    #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none)
    1.32 -  |> reset_pos pos;
    1.33 +  |> reset_range pos;
    1.34  
    1.35  fun make_src a args = make_string a :: args;
    1.36