src/Pure/Tools/rail.ML
changeset 59064 a8bcb5a446c8
parent 59058 a78612c67ec0
child 59809 87641097d0f3
     1.1 --- a/src/Pure/Tools/rail.ML	Sat Nov 29 14:43:10 2014 +0100
     1.2 +++ b/src/Pure/Tools/rail.ML	Sun Nov 30 12:24:56 2014 +0100
     1.3 @@ -281,11 +281,10 @@
     1.4  
     1.5  (* read *)
     1.6  
     1.7 -fun read ctxt (source: Symbol_Pos.source) =
     1.8 +fun read ctxt source =
     1.9    let
    1.10 -    val {text, range = (pos, _), ...} = source;
    1.11 -    val _ = Context_Position.report ctxt pos Markup.language_rail;
    1.12 -    val toks = tokenize (Symbol_Pos.explode (text, pos));
    1.13 +    val _ = Context_Position.report ctxt (Input.pos_of source) Markup.language_rail;
    1.14 +    val toks = tokenize (Input.source_explode source);
    1.15      val _ = Context_Position.reports ctxt (maps reports_of_token toks);
    1.16      val rules = parse_rules toks;
    1.17      val _ = Position.reports (maps (reports_of_tree ctxt o #2) rules);