--- a/src/Pure/Syntax/syntax_phases.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Tue Nov 11 18:16:25 2014 +0100
@@ -462,10 +462,11 @@
| decode ps (Ast.Appl asts) = decode_appl ps asts;
val source = Syntax.read_token str;
+ val (pos, _) = #range source;
val syms = Symbol_Pos.source_explode source;
val ast =
- parse_asts ctxt true root (syms, #pos source)
- |> uncurry (report_result ctxt (#pos source))
+ parse_asts ctxt true root (syms, pos)
+ |> uncurry (report_result ctxt pos)
|> decode [];
val _ = Context_Position.reports_text ctxt (! reports);
in ast end;