--- a/src/Pure/Tools/rail.ML Sat Mar 01 19:55:01 2014 +0100
+++ b/src/Pure/Tools/rail.ML Sat Mar 01 22:46:31 2014 +0100
@@ -192,10 +192,11 @@
in
-fun read ctxt (s, pos) =
+fun read ctxt (source: Symbol_Pos.source) =
let
+ val {text, pos, ...} = source;
val _ = Context_Position.report ctxt pos Markup.language_rail;
- val toks = tokenize (Symbol_Pos.explode (s, pos));
+ val toks = tokenize (Symbol_Pos.explode (text, pos));
val _ = Context_Position.reports ctxt (maps reports_of_token toks);
in #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks) end;