src/Pure/Tools/rail.ML
changeset 58978 e42da880c61e
parent 58928 23d0ffd48006
child 59058 a78612c67ec0
     1.1 --- a/src/Pure/Tools/rail.ML	Tue Nov 11 15:55:31 2014 +0100
     1.2 +++ b/src/Pure/Tools/rail.ML	Tue Nov 11 18:16:25 2014 +0100
     1.3 @@ -283,7 +283,7 @@
     1.4  
     1.5  fun read ctxt (source: Symbol_Pos.source) =
     1.6    let
     1.7 -    val {text, pos, ...} = source;
     1.8 +    val {text, range = (pos, _), ...} = source;
     1.9      val _ = Context_Position.report ctxt pos Markup.language_rail;
    1.10      val toks = tokenize (Symbol_Pos.explode (text, pos));
    1.11      val _ = Context_Position.reports ctxt (maps reports_of_token toks);