# HG changeset patch
# User wenzelm
# Date 1415726185 -3600
# Node ID e42da880c61ea1d88025b192bf2c386de548636b
# Parent  9576b510f6a268f2e745902a5b11952bfb68ab06
more position information, e.g. relevant for errors in generated ML source;

diff -r 9576b510f6a2 -r e42da880c61e src/Doc/antiquote_setup.ML
--- 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);
diff -r 9576b510f6a2 -r e42da880c61e src/HOL/ex/Cartouche_Examples.thy
--- 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;
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/General/position.ML
--- 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 *)
 
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/General/symbol_pos.ML
--- 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;
 
 
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/Isar/attrib.ML
--- 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;
 
 
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/Isar/isar_cmd.ML
--- 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, \
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/Isar/isar_syn.ML
--- 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
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/Isar/method.ML
--- 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;
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/Isar/token.ML
--- 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;
 
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/ML/ml_antiquotations.ML
--- 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 *)
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/ML/ml_context.ML
--- 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;
 
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/ML/ml_file.ML
--- 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
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/ML/ml_lex.ML
--- 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 _ =
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/ML/ml_syntax.ML
--- 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;
 
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/PIDE/markup.ML
--- 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";
 
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/PIDE/markup.scala
--- 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"
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/Syntax/syntax.ML
--- 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, _), _)] =>
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/Syntax/syntax_phases.ML
--- 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;
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/Thy/latex.ML
--- 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
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/Thy/thy_output.ML
--- 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));
 
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/Thy/thy_syntax.ML
--- 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) =>
diff -r 9576b510f6a2 -r e42da880c61e src/Pure/Tools/rail.ML
--- 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);