src/Pure/Tools/rail.ML
changeset 55828 42ac3cfb89f6
parent 55613 ad446b45efff
child 56163 331f4aba14b3
     1.1 --- a/src/Pure/Tools/rail.ML	Sat Mar 01 19:55:01 2014 +0100
     1.2 +++ b/src/Pure/Tools/rail.ML	Sat Mar 01 22:46:31 2014 +0100
     1.3 @@ -192,10 +192,11 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun read ctxt (s, pos) =
     1.8 +fun read ctxt (source: Symbol_Pos.source) =
     1.9    let
    1.10 +    val {text, pos, ...} = source;
    1.11      val _ = Context_Position.report ctxt pos Markup.language_rail;
    1.12 -    val toks = tokenize (Symbol_Pos.explode (s, pos));
    1.13 +    val toks = tokenize (Symbol_Pos.explode (text, pos));
    1.14      val _ = Context_Position.reports ctxt (maps reports_of_token toks);
    1.15    in #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks) end;
    1.16