more position information, e.g. relevant for errors in generated ML source;
--- a/src/Doc/antiquote_setup.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Tue Nov 11 18:16:25 2014 +0100
@@ -90,7 +90,7 @@
else txt1 ^ " : " ^ txt2;
val txt' = if kind = "" then txt else kind ^ " " ^ txt;
- val pos = #pos source1;
+ val (pos, _) = #range source1;
val _ =
ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2))
handle ERROR msg => error (msg ^ Position.here pos);
--- a/src/HOL/ex/Cartouche_Examples.thy Tue Nov 11 15:55:31 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Tue Nov 11 18:16:25 2014 +0100
@@ -146,7 +146,8 @@
ML_Lex.read Position.none "fn _ => (" @
ML_Lex.read_source false source @
ML_Lex.read Position.none ");";
- val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) toks;
+ val (pos, _) = #range source;
+ val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags pos toks;
in "" end);
*}
@@ -213,7 +214,7 @@
fun ml_tactic source ctxt =
let
val ctxt' = ctxt |> Context.proof_map
- (ML_Context.expression (#pos source)
+ (ML_Context.expression (#range source)
"fun tactic (ctxt : Proof.context) : tactic"
"Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source false source));
in Data.get ctxt' ctxt end;
--- a/src/Pure/General/position.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/General/position.ML Tue Nov 11 18:16:25 2014 +0100
@@ -53,6 +53,8 @@
val set_range: range -> T
val reset_range: T -> T
val range: T -> T -> range
+ val range_of_properties: Properties.T -> range
+ val properties_of_range: range -> Properties.T
val thread_data: unit -> T
val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
val default: T -> bool * T
@@ -134,17 +136,16 @@
(* markup properties *)
+fun get props name =
+ (case Properties.get props name of
+ NONE => 0
+ | SOME s => Markup.parse_int s);
+
fun of_properties props =
- let
- fun get name =
- (case Properties.get props name of
- NONE => 0
- | SOME s => Markup.parse_int s);
- in
- make {line = get Markup.lineN, offset = get Markup.offsetN,
- end_offset = get Markup.end_offsetN, props = props}
- end;
-
+ make {line = get props Markup.lineN,
+ offset = get props Markup.offsetN,
+ end_offset = get props Markup.end_offsetN,
+ props = props};
fun value k i = if valid i then [(k, Markup.print_int i)] else [];
@@ -221,6 +222,19 @@
fun range pos pos' = (set_range (pos, pos'), pos');
+fun range_of_properties props =
+ let
+ val pos = of_properties props;
+ val pos' =
+ make {line = get props Markup.end_lineN,
+ offset = get props Markup.end_offsetN,
+ end_offset = 0,
+ props = props};
+ in (pos, pos') end;
+
+fun properties_of_range (pos, pos') =
+ properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos'));
+
(* thread data *)
--- a/src/Pure/General/symbol_pos.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML Tue Nov 11 18:16:25 2014 +0100
@@ -39,7 +39,7 @@
val implode: T list -> text
val implode_range: Position.T -> Position.T -> T list -> text * Position.range
val explode: text * Position.T -> T list
- type source = {delimited: bool, text: text, pos: Position.T}
+ type source = {delimited: bool, text: text, range: Position.range}
val source_explode: source -> T list
val source_content: source -> string * Position.T
val scan_ident: T list -> T list * T list
@@ -255,11 +255,11 @@
(* full source information *)
-type source = {delimited: bool, text: text, pos: Position.T};
+type source = {delimited: bool, text: text, range: Position.range};
-fun source_explode {delimited = _, text, pos} = explode (text, pos);
+fun source_explode {delimited = _, text, range = (pos, _)} = explode (text, pos);
-fun source_content {delimited = _, text, pos} =
+fun source_content {delimited = _, text, range = (pos, _)} =
let val syms = explode (text, pos) in (content syms, pos) end;
--- a/src/Pure/Isar/attrib.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Nov 11 18:16:25 2014 +0100
@@ -210,7 +210,7 @@
(ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
ML_Lex.read_source false source @
ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
- |> ML_Context.expression (#pos source)
+ |> ML_Context.expression (#range source)
"val (name, scan, comment): binding * attribute context_parser * string"
"Context.map_proof (Attrib.local_setup name scan comment)"
|> Context.proof_map;
@@ -293,7 +293,7 @@
in
(case Token.read_no_commands keywords Parse.attribs syms of
[raw_srcs] => check_attribs ctxt raw_srcs
- | _ => error ("Malformed attributes" ^ Position.here (#pos source)))
+ | _ => error ("Malformed attributes" ^ Position.here (#1 (#range source))))
end;
--- a/src/Pure/Isar/isar_cmd.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Tue Nov 11 18:16:25 2014 +0100
@@ -60,12 +60,14 @@
fun global_setup source =
ML_Lex.read_source false source
- |> ML_Context.expression (#pos source) "val setup: theory -> theory" "Context.map_theory setup"
+ |> ML_Context.expression (#range source)
+ "val setup: theory -> theory" "Context.map_theory setup"
|> Context.theory_map;
fun local_setup source =
ML_Lex.read_source false source
- |> ML_Context.expression (#pos source) "val setup: local_theory -> local_theory" "Context.map_proof setup"
+ |> ML_Context.expression (#range source)
+ "val setup: local_theory -> local_theory" "Context.map_proof setup"
|> Context.proof_map;
@@ -73,35 +75,35 @@
fun parse_ast_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#pos source)
+ |> ML_Context.expression (#range source)
"val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
"Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
|> Context.theory_map;
fun parse_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#pos source)
+ |> ML_Context.expression (#range source)
"val parse_translation: (string * (Proof.context -> term list -> term)) list"
"Context.map_theory (Sign.parse_translation parse_translation)"
|> Context.theory_map;
fun print_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#pos source)
+ |> ML_Context.expression (#range source)
"val print_translation: (string * (Proof.context -> term list -> term)) list"
"Context.map_theory (Sign.print_translation print_translation)"
|> Context.theory_map;
fun typed_print_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#pos source)
+ |> ML_Context.expression (#range source)
"val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
"Context.map_theory (Sign.typed_print_translation typed_print_translation)"
|> Context.theory_map;
fun print_ast_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#pos source)
+ |> ML_Context.expression (#range source)
"val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
"Context.map_theory (Sign.print_ast_translation print_ast_translation)"
|> Context.theory_map;
@@ -139,7 +141,7 @@
\end;\n");
in
Context.theory_map
- (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#pos source) ants))
+ (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#1 (#range source)) ants))
end;
@@ -158,7 +160,7 @@
fun declaration {syntax, pervasive} source =
ML_Lex.read_source false source
- |> ML_Context.expression (#pos source)
+ |> ML_Context.expression (#range source)
"val declaration: Morphism.declaration"
("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
\pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
@@ -169,7 +171,7 @@
fun simproc_setup name lhss source identifier =
ML_Lex.read_source false source
- |> ML_Context.expression (#pos source)
+ |> ML_Context.expression (#range source)
"val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
\lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
--- a/src/Pure/Isar/isar_syn.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Tue Nov 11 18:16:25 2014 +0100
@@ -232,7 +232,7 @@
(Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
let
val ([{lines, pos, ...}], thy') = files thy;
- val source = {delimited = true, text = cat_lines lines, pos = pos};
+ val source = {delimited = true, text = cat_lines lines, range = (pos, pos)};
val flags = {SML = true, exchange = false, redirect = true, verbose = true};
in
thy' |> Context.theory_map
--- a/src/Pure/Isar/method.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Isar/method.ML Tue Nov 11 18:16:25 2014 +0100
@@ -282,7 +282,7 @@
Scan.lift (Args.text_declaration (fn source =>
let
val context' = context |>
- ML_Context.expression (#pos source)
+ ML_Context.expression (#range source)
"fun tactic (morphism: Morphism.morphism) (facts: thm list) : tactic"
"Method.set_tactic tactic" (ML_Lex.read_source false source);
val tac = the_tactic context';
@@ -381,7 +381,7 @@
(ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
ML_Lex.read_source false source @
ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
- |> ML_Context.expression (#pos source)
+ |> ML_Context.expression (#range source)
"val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
"Context.map_proof (Method.local_setup name scan comment)"
|> Context.proof_map;
--- a/src/Pure/Isar/token.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Isar/token.ML Tue Nov 11 18:16:25 2014 +0100
@@ -268,8 +268,8 @@
val tree = XML.Elem (Markup.token delimited (Position.properties_of pos), [XML.Text source]);
in YXML.string_of tree end;
-fun source_position_of (Token ((source, (pos, _)), (kind, _), _)) =
- {delimited = delimited_kind kind, text = source, pos = pos};
+fun source_position_of (Token ((source, range), (kind, _), _)) =
+ {delimited = delimited_kind kind, text = source, range = range};
fun content_of (Token (_, (_, x), _)) = x;
--- a/src/Pure/ML/ml_antiquotations.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Tue Nov 11 18:16:25 2014 +0100
@@ -34,10 +34,10 @@
val _ = Theory.setup
(ML_Antiquotation.value @{binding source}
- (Scan.lift Args.text_source_position >> (fn {delimited, text, pos} =>
+ (Scan.lift Args.text_source_position >> (fn {delimited, text, range} =>
"{delimited = " ^ Bool.toString delimited ^
", text = " ^ ML_Syntax.print_string text ^
- ", pos = " ^ ML_Syntax.print_position pos ^ "}")));
+ ", range = " ^ ML_Syntax.print_range range ^ "}")));
(* formal entities *)
--- a/src/Pure/ML/ml_context.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/ML/ml_context.ML Tue Nov 11 18:16:25 2014 +0100
@@ -25,8 +25,8 @@
val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
ML_Lex.token Antiquote.antiquote list -> unit
val eval_source_in: Proof.context option -> ML_Compiler.flags -> Symbol_Pos.source -> unit
- val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
- Context.generic -> Context.generic
+ val expression: Position.range -> string -> string ->
+ ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
end
structure ML_Context: ML_CONTEXT =
@@ -173,7 +173,7 @@
in eval flags pos (ML_Lex.read pos (File.read path)) end;
fun eval_source flags source =
- eval flags (#pos source) (ML_Lex.read_source (#SML flags) source);
+ eval flags (#1 (#range source)) (ML_Lex.read_source (#SML flags) source);
fun eval_in ctxt flags pos ants =
Context.setmp_thread_data (Option.map Context.Proof ctxt)
@@ -183,11 +183,12 @@
Context.setmp_thread_data (Option.map Context.Proof ctxt)
(fn () => eval_source flags source) ();
-fun expression pos bind body ants =
+fun expression range bind body ants =
exec (fn () =>
- eval ML_Compiler.flags pos
- (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
- ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
+ eval ML_Compiler.flags (#1 range)
+ (ML_Lex.read_set_range range ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @
+ ants @
+ ML_Lex.read_set_range range (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
end;
--- a/src/Pure/ML/ml_file.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/ML/ml_file.ML Tue Nov 11 18:16:25 2014 +0100
@@ -13,7 +13,7 @@
let
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
val provide = Resources.provide (src_path, digest);
- val source = {delimited = true, text = cat_lines lines, pos = pos};
+ val source = {delimited = true, text = cat_lines lines, range = (pos, pos)};
val flags = {SML = false, exchange = false, redirect = true, verbose = true};
in
gthy
--- a/src/Pure/ML/ml_lex.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Tue Nov 11 18:16:25 2014 +0100
@@ -26,6 +26,7 @@
Source.source) Source.source
val tokenize: string -> token list
val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
+ val read_set_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list
val read_source: bool -> Symbol_Pos.source -> token Antiquote.antiquote list
end;
@@ -325,7 +326,11 @@
val read = gen_read false;
-fun read_source SML {delimited, text, pos} =
+fun read_set_range range =
+ read Position.none
+ #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq);
+
+fun read_source SML ({delimited, text, range = (pos, _)}: Symbol_Pos.source) =
let
val language = if SML then Markup.language_SML else Markup.language_ML;
val _ =
--- a/src/Pure/ML/ml_syntax.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/ML/ml_syntax.ML Tue Nov 11 18:16:25 2014 +0100
@@ -20,6 +20,7 @@
val print_strings: string list -> string
val print_properties: Properties.T -> string
val print_position: Position.T -> string
+ val print_range: Position.range -> string
val make_binding: string * Position.T -> string
val print_indexname: indexname -> string
val print_class: class -> string
@@ -77,8 +78,15 @@
val print_strings = print_list print_string;
val print_properties = print_list (print_pair print_string print_string);
-fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
-fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos);
+
+fun print_position pos =
+ "Position.of_properties " ^ print_properties (Position.properties_of pos);
+
+fun print_range range =
+ "Position.range_of_properties " ^ print_properties (Position.properties_of_range range);
+
+fun make_binding (name, pos) =
+ "Binding.make " ^ print_pair print_string print_position (name, pos);
val print_indexname = print_pair print_string print_int;
--- a/src/Pure/PIDE/markup.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Tue Nov 11 18:16:25 2014 +0100
@@ -47,6 +47,7 @@
val completionN: string val completion: T
val no_completionN: string val no_completion: T
val lineN: string
+ val end_lineN: string
val offsetN: string
val end_offsetN: string
val fileN: string
@@ -329,8 +330,11 @@
(* position *)
val lineN = "line";
+val end_lineN = "end_line";
+
val offsetN = "offset";
val end_offsetN = "end_offset";
+
val fileN = "file";
val idN = "id";
--- a/src/Pure/PIDE/markup.scala Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Tue Nov 11 18:16:25 2014 +0100
@@ -100,6 +100,7 @@
/* position */
val LINE = "line"
+ val END_LINE = "line"
val OFFSET = "offset"
val END_OFFSET = "end_offset"
val FILE = "file"
--- a/src/Pure/Syntax/syntax.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Syntax/syntax.ML Tue Nov 11 18:16:25 2014 +0100
@@ -163,21 +163,21 @@
local
-fun token_position (XML.Elem ((name, props), _)) =
+fun token_range (XML.Elem ((name, props), _)) =
if name = Markup.tokenN
- then (Markup.is_delimited props, Position.of_properties props)
- else (false, Position.none)
- | token_position (XML.Text _) = (false, Position.none);
+ then (Markup.is_delimited props, Position.range_of_properties props)
+ else (false, Position.no_range)
+ | token_range (XML.Text _) = (false, Position.no_range);
-fun token_source tree =
+fun token_source tree : Symbol_Pos.source =
let
val text = XML.content_of [tree];
- val (delimited, pos) = token_position tree;
- in {delimited = delimited, text = text, pos = pos} end;
+ val (delimited, range) = token_range tree;
+ in {delimited = delimited, text = text, range = range} end;
in
-fun read_token_pos str = #2 (token_position (YXML.parse str handle Fail msg => error msg));
+fun read_token_pos str = #1 (#2 (token_range (YXML.parse str handle Fail msg => error msg)));
fun read_token str = token_source (YXML.parse str handle Fail msg => error msg);
@@ -187,8 +187,9 @@
let
val source = token_source tree;
val syms = Symbol_Pos.source_explode source;
- val _ = Context_Position.report ctxt (#pos source) (markup (#delimited source));
- in parse (syms, #pos source) end;
+ val (pos, _) = #range source;
+ val _ = Context_Position.report ctxt pos (markup (#delimited source));
+ in parse (syms, pos) end;
in
(case YXML.parse_body str handle Fail msg => error msg of
body as [tree as XML.Elem ((name, _), _)] =>
--- 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;
--- a/src/Pure/Thy/latex.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Thy/latex.ML Tue Nov 11 18:16:25 2014 +0100
@@ -132,7 +132,7 @@
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
else if Token.is_kind Token.Verbatim tok then
let
- val {text, pos, ...} = Token.source_position_of tok;
+ val {text, range = (pos, _), ...} = Token.source_position_of tok;
val ants = Antiquote.read (Symbol_Pos.explode (text, pos), pos);
val out = implode (map output_syms_antiq ants);
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
--- a/src/Pure/Thy/thy_output.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue Nov 11 18:16:25 2014 +0100
@@ -195,10 +195,10 @@
val _ = Position.reports (maps words ants);
in implode (map expand ants) end;
-fun check_text {delimited, text, pos} state =
- (Position.report pos (Markup.language_document delimited);
+fun check_text {delimited, text, range} state =
+ (Position.report (fst range) (Markup.language_document delimited);
if Toplevel.is_skipped_proof state then ()
- else ignore (eval_antiquote state (text, pos)));
+ else ignore (eval_antiquote state (text, fst range)));
@@ -372,7 +372,7 @@
Parse.position (Scan.one (Token.is_command andf is_markup mark o Token.content_of)) --
Scan.repeat tag --
Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
- >> (fn (((tok, pos'), tags), {text, pos, ...}) =>
+ >> (fn (((tok, pos'), tags), {text, range = (pos, _), ...}) =>
let val name = Token.content_of tok
in (SOME (name, pos', tags), (mk (name, (text, pos)), (flag, d))) end));
@@ -385,7 +385,7 @@
val cmt = Scan.peek (fn d =>
Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source)
- >> (fn {text, pos, ...} => (NONE, (MarkupToken ("cmt", (text, pos)), ("", d)))));
+ >> (fn {text, range = (pos, _), ...} => (NONE, (MarkupToken ("cmt", (text, pos)), ("", d)))));
val other = Scan.peek (fn d =>
Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
@@ -482,7 +482,7 @@
fun pretty_text_report ctxt source =
let
- val {delimited, pos, ...} = source;
+ val {delimited, range = (pos, _), ...} = source;
val _ = Context_Position.report ctxt pos (Markup.language_text delimited);
val (s, _) = Symbol_Pos.source_content source;
in pretty_text ctxt s end;
@@ -664,7 +664,7 @@
fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position)
(fn {context = ctxt, ...} => fn source =>
- (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source) (ml source);
+ (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#1 (#range source)) (ml source);
Symbol_Pos.source_content source |> #1
|> verbatim_text ctxt));
--- a/src/Pure/Thy/thy_syntax.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Tue Nov 11 18:16:25 2014 +0100
@@ -26,7 +26,7 @@
fun reports_of_token tok =
let
- val {text, pos, ...} = Token.source_position_of tok;
+ val {text, range = (pos, _), ...} = Token.source_position_of tok;
val malformed_symbols =
Symbol_Pos.explode (text, pos)
|> map_filter (fn (sym, pos) =>
--- 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);