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