src/Pure/Tools/rail.ML
changeset 62797 e08c44eed27f
parent 62748 aa0084adce1f
child 62806 de9bf8171626
     1.1 --- a/src/Pure/Tools/rail.ML	Fri Apr 01 17:23:15 2016 +0200
     1.2 +++ b/src/Pure/Tools/rail.ML	Fri Apr 01 17:37:46 2016 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4  
     1.5  fun range_of (toks as tok :: _) =
     1.6        let val pos' = end_pos_of (List.last toks)
     1.7 -      in Position.range (pos_of tok) pos' end
     1.8 +      in Position.range (pos_of tok, pos') end
     1.9    | range_of [] = Position.no_range;
    1.10  
    1.11  fun kind_of (Token (_, (k, _))) = k;
    1.12 @@ -116,7 +116,7 @@
    1.13    scan_keyword >> (token Keyword o single) ||
    1.14    Lexicon.scan_id >> token Ident ||
    1.15    Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
    1.16 -    [Token (Position.range pos1 pos2, (String, Symbol_Pos.content ss))]);
    1.17 +    [Token (Position.range (pos1, pos2), (String, Symbol_Pos.content ss))]);
    1.18  
    1.19  val scan =
    1.20    Scan.repeats scan_token --|
    1.21 @@ -188,7 +188,7 @@
    1.22      let
    1.23        fun reports r =
    1.24          if r = Position.no_range then []
    1.25 -        else [(Position.set_range r, Markup.expression)];
    1.26 +        else [(Position.range_position r, Markup.expression)];
    1.27        fun trees (CAT (ts, r)) = reports r @ maps tree ts
    1.28        and tree (BAR (Ts, r)) = reports r @ maps trees Ts
    1.29          | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2