--- a/src/Pure/Tools/rail.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Tools/rail.ML Sun Nov 30 12:24:56 2014 +0100
@@ -281,11 +281,10 @@
(* read *)
-fun read ctxt (source: Symbol_Pos.source) =
+fun read ctxt source =
let
- 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.report ctxt (Input.pos_of source) Markup.language_rail;
+ val toks = tokenize (Input.source_explode source);
val _ = Context_Position.reports ctxt (maps reports_of_token toks);
val rules = parse_rules toks;
val _ = Position.reports (maps (reports_of_tree ctxt o #2) rules);