more position information, e.g. relevant for errors in generated ML source;
authorwenzelm
Tue Nov 11 18:16:25 2014 +0100 (2014-11-11 ago)
changeset 58978e42da880c61e
parent 58977 9576b510f6a2
child 58979 162a4c2e97bc
more position information, e.g. relevant for errors in generated ML source;
src/Doc/antiquote_setup.ML
src/HOL/ex/Cartouche_Examples.thy
src/Pure/General/position.ML
src/Pure/General/symbol_pos.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/method.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_file.ML
src/Pure/ML/ml_lex.ML
src/Pure/ML/ml_syntax.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
src/Pure/Thy/thy_syntax.ML
src/Pure/Tools/rail.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Tue Nov 11 15:55:31 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Tue Nov 11 18:16:25 2014 +0100
     1.3 @@ -90,7 +90,7 @@
     1.4          else txt1 ^ " : " ^ txt2;
     1.5        val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     1.6  
     1.7 -      val pos = #pos source1;
     1.8 +      val (pos, _) = #range source1;
     1.9        val _ =
    1.10          ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2))
    1.11            handle ERROR msg => error (msg ^ Position.here pos);
     2.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Tue Nov 11 15:55:31 2014 +0100
     2.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Nov 11 18:16:25 2014 +0100
     2.3 @@ -146,7 +146,8 @@
     2.4            ML_Lex.read Position.none "fn _ => (" @
     2.5            ML_Lex.read_source false source @
     2.6            ML_Lex.read Position.none ");";
     2.7 -        val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) toks;
     2.8 +        val (pos, _) = #range source;
     2.9 +        val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags pos toks;
    2.10        in "" end);
    2.11  *}
    2.12  
    2.13 @@ -213,7 +214,7 @@
    2.14    fun ml_tactic source ctxt =
    2.15      let
    2.16        val ctxt' = ctxt |> Context.proof_map
    2.17 -        (ML_Context.expression (#pos source)
    2.18 +        (ML_Context.expression (#range source)
    2.19            "fun tactic (ctxt : Proof.context) : tactic"
    2.20            "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source false source));
    2.21      in Data.get ctxt' ctxt end;
     3.1 --- a/src/Pure/General/position.ML	Tue Nov 11 15:55:31 2014 +0100
     3.2 +++ b/src/Pure/General/position.ML	Tue Nov 11 18:16:25 2014 +0100
     3.3 @@ -53,6 +53,8 @@
     3.4    val set_range: range -> T
     3.5    val reset_range: T -> T
     3.6    val range: T -> T -> range
     3.7 +  val range_of_properties: Properties.T -> range
     3.8 +  val properties_of_range: range -> Properties.T
     3.9    val thread_data: unit -> T
    3.10    val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
    3.11    val default: T -> bool * T
    3.12 @@ -134,17 +136,16 @@
    3.13  
    3.14  (* markup properties *)
    3.15  
    3.16 +fun get props name =
    3.17 +  (case Properties.get props name of
    3.18 +    NONE => 0
    3.19 +  | SOME s => Markup.parse_int s);
    3.20 +
    3.21  fun of_properties props =
    3.22 -  let
    3.23 -    fun get name =
    3.24 -      (case Properties.get props name of
    3.25 -        NONE => 0
    3.26 -      | SOME s => Markup.parse_int s);
    3.27 -  in
    3.28 -    make {line = get Markup.lineN, offset = get Markup.offsetN,
    3.29 -      end_offset = get Markup.end_offsetN, props = props}
    3.30 -  end;
    3.31 -
    3.32 +  make {line = get props Markup.lineN,
    3.33 +    offset = get props Markup.offsetN,
    3.34 +    end_offset = get props Markup.end_offsetN,
    3.35 +    props = props};
    3.36  
    3.37  fun value k i = if valid i then [(k, Markup.print_int i)] else [];
    3.38  
    3.39 @@ -221,6 +222,19 @@
    3.40  
    3.41  fun range pos pos' = (set_range (pos, pos'), pos');
    3.42  
    3.43 +fun range_of_properties props =
    3.44 +  let
    3.45 +    val pos = of_properties props;
    3.46 +    val pos' =
    3.47 +      make {line = get props Markup.end_lineN,
    3.48 +        offset = get props Markup.end_offsetN,
    3.49 +        end_offset = 0,
    3.50 +        props = props};
    3.51 +  in (pos, pos') end;
    3.52 +
    3.53 +fun properties_of_range (pos, pos') =
    3.54 +  properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos'));
    3.55 +
    3.56  
    3.57  (* thread data *)
    3.58  
     4.1 --- a/src/Pure/General/symbol_pos.ML	Tue Nov 11 15:55:31 2014 +0100
     4.2 +++ b/src/Pure/General/symbol_pos.ML	Tue Nov 11 18:16:25 2014 +0100
     4.3 @@ -39,7 +39,7 @@
     4.4    val implode: T list -> text
     4.5    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
     4.6    val explode: text * Position.T -> T list
     4.7 -  type source = {delimited: bool, text: text, pos: Position.T}
     4.8 +  type source = {delimited: bool, text: text, range: Position.range}
     4.9    val source_explode: source -> T list
    4.10    val source_content: source -> string * Position.T
    4.11    val scan_ident: T list -> T list * T list
    4.12 @@ -255,11 +255,11 @@
    4.13  
    4.14  (* full source information *)
    4.15  
    4.16 -type source = {delimited: bool, text: text, pos: Position.T};
    4.17 +type source = {delimited: bool, text: text, range: Position.range};
    4.18  
    4.19 -fun source_explode {delimited = _, text, pos} = explode (text, pos);
    4.20 +fun source_explode {delimited = _, text, range = (pos, _)} = explode (text, pos);
    4.21  
    4.22 -fun source_content {delimited = _, text, pos} =
    4.23 +fun source_content {delimited = _, text, range = (pos, _)} =
    4.24    let val syms = explode (text, pos) in (content syms, pos) end;
    4.25  
    4.26  
     5.1 --- a/src/Pure/Isar/attrib.ML	Tue Nov 11 15:55:31 2014 +0100
     5.2 +++ b/src/Pure/Isar/attrib.ML	Tue Nov 11 18:16:25 2014 +0100
     5.3 @@ -210,7 +210,7 @@
     5.4    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
     5.5      ML_Lex.read_source false source @
     5.6      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
     5.7 -  |> ML_Context.expression (#pos source)
     5.8 +  |> ML_Context.expression (#range source)
     5.9      "val (name, scan, comment): binding * attribute context_parser * string"
    5.10      "Context.map_proof (Attrib.local_setup name scan comment)"
    5.11    |> Context.proof_map;
    5.12 @@ -293,7 +293,7 @@
    5.13    in
    5.14      (case Token.read_no_commands keywords Parse.attribs syms of
    5.15        [raw_srcs] => check_attribs ctxt raw_srcs
    5.16 -    | _ => error ("Malformed attributes" ^ Position.here (#pos source)))
    5.17 +    | _ => error ("Malformed attributes" ^ Position.here (#1 (#range source))))
    5.18    end;
    5.19  
    5.20  
     6.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 11 15:55:31 2014 +0100
     6.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Nov 11 18:16:25 2014 +0100
     6.3 @@ -60,12 +60,14 @@
     6.4  
     6.5  fun global_setup source =
     6.6    ML_Lex.read_source false source
     6.7 -  |> ML_Context.expression (#pos source) "val setup: theory -> theory" "Context.map_theory setup"
     6.8 +  |> ML_Context.expression (#range source)
     6.9 +    "val setup: theory -> theory" "Context.map_theory setup"
    6.10    |> Context.theory_map;
    6.11  
    6.12  fun local_setup source =
    6.13    ML_Lex.read_source false source
    6.14 -  |> ML_Context.expression (#pos source) "val setup: local_theory -> local_theory" "Context.map_proof setup"
    6.15 +  |> ML_Context.expression (#range source)
    6.16 +    "val setup: local_theory -> local_theory" "Context.map_proof setup"
    6.17    |> Context.proof_map;
    6.18  
    6.19  
    6.20 @@ -73,35 +75,35 @@
    6.21  
    6.22  fun parse_ast_translation source =
    6.23    ML_Lex.read_source false source
    6.24 -  |> ML_Context.expression (#pos source)
    6.25 +  |> ML_Context.expression (#range source)
    6.26      "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    6.27      "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    6.28    |> Context.theory_map;
    6.29  
    6.30  fun parse_translation source =
    6.31    ML_Lex.read_source false source
    6.32 -  |> ML_Context.expression (#pos source)
    6.33 +  |> ML_Context.expression (#range source)
    6.34      "val parse_translation: (string * (Proof.context -> term list -> term)) list"
    6.35      "Context.map_theory (Sign.parse_translation parse_translation)"
    6.36    |> Context.theory_map;
    6.37  
    6.38  fun print_translation source =
    6.39    ML_Lex.read_source false source
    6.40 -  |> ML_Context.expression (#pos source)
    6.41 +  |> ML_Context.expression (#range source)
    6.42      "val print_translation: (string * (Proof.context -> term list -> term)) list"
    6.43      "Context.map_theory (Sign.print_translation print_translation)"
    6.44    |> Context.theory_map;
    6.45  
    6.46  fun typed_print_translation source =
    6.47    ML_Lex.read_source false source
    6.48 -  |> ML_Context.expression (#pos source)
    6.49 +  |> ML_Context.expression (#range source)
    6.50      "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
    6.51      "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
    6.52    |> Context.theory_map;
    6.53  
    6.54  fun print_ast_translation source =
    6.55    ML_Lex.read_source false source
    6.56 -  |> ML_Context.expression (#pos source)
    6.57 +  |> ML_Context.expression (#range source)
    6.58      "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    6.59      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
    6.60    |> Context.theory_map;
    6.61 @@ -139,7 +141,7 @@
    6.62          \end;\n");
    6.63    in
    6.64      Context.theory_map
    6.65 -      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#pos source) ants))
    6.66 +      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#1 (#range source)) ants))
    6.67    end;
    6.68  
    6.69  
    6.70 @@ -158,7 +160,7 @@
    6.71  
    6.72  fun declaration {syntax, pervasive} source =
    6.73    ML_Lex.read_source false source
    6.74 -  |> ML_Context.expression (#pos source)
    6.75 +  |> ML_Context.expression (#range source)
    6.76      "val declaration: Morphism.declaration"
    6.77      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
    6.78        \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
    6.79 @@ -169,7 +171,7 @@
    6.80  
    6.81  fun simproc_setup name lhss source identifier =
    6.82    ML_Lex.read_source false source
    6.83 -  |> ML_Context.expression (#pos source)
    6.84 +  |> ML_Context.expression (#range source)
    6.85      "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
    6.86      ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
    6.87        \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
     7.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Nov 11 15:55:31 2014 +0100
     7.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 11 18:16:25 2014 +0100
     7.3 @@ -232,7 +232,7 @@
     7.4      (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
     7.5          let
     7.6            val ([{lines, pos, ...}], thy') = files thy;
     7.7 -          val source = {delimited = true, text = cat_lines lines, pos = pos};
     7.8 +          val source = {delimited = true, text = cat_lines lines, range = (pos, pos)};
     7.9            val flags = {SML = true, exchange = false, redirect = true, verbose = true};
    7.10          in
    7.11            thy' |> Context.theory_map
     8.1 --- a/src/Pure/Isar/method.ML	Tue Nov 11 15:55:31 2014 +0100
     8.2 +++ b/src/Pure/Isar/method.ML	Tue Nov 11 18:16:25 2014 +0100
     8.3 @@ -282,7 +282,7 @@
     8.4      Scan.lift (Args.text_declaration (fn source =>
     8.5        let
     8.6          val context' = context |>
     8.7 -          ML_Context.expression (#pos source)
     8.8 +          ML_Context.expression (#range source)
     8.9              "fun tactic (morphism: Morphism.morphism) (facts: thm list) : tactic"
    8.10              "Method.set_tactic tactic" (ML_Lex.read_source false source);
    8.11          val tac = the_tactic context';
    8.12 @@ -381,7 +381,7 @@
    8.13    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
    8.14      ML_Lex.read_source false source @
    8.15      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
    8.16 -  |> ML_Context.expression (#pos source)
    8.17 +  |> ML_Context.expression (#range source)
    8.18      "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
    8.19      "Context.map_proof (Method.local_setup name scan comment)"
    8.20    |> Context.proof_map;
     9.1 --- a/src/Pure/Isar/token.ML	Tue Nov 11 15:55:31 2014 +0100
     9.2 +++ b/src/Pure/Isar/token.ML	Tue Nov 11 18:16:25 2014 +0100
     9.3 @@ -268,8 +268,8 @@
     9.4        val tree = XML.Elem (Markup.token delimited (Position.properties_of pos), [XML.Text source]);
     9.5      in YXML.string_of tree end;
     9.6  
     9.7 -fun source_position_of (Token ((source, (pos, _)), (kind, _), _)) =
     9.8 -  {delimited = delimited_kind kind, text = source, pos = pos};
     9.9 +fun source_position_of (Token ((source, range), (kind, _), _)) =
    9.10 +  {delimited = delimited_kind kind, text = source, range = range};
    9.11  
    9.12  fun content_of (Token (_, (_, x), _)) = x;
    9.13  
    10.1 --- a/src/Pure/ML/ml_antiquotations.ML	Tue Nov 11 15:55:31 2014 +0100
    10.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Tue Nov 11 18:16:25 2014 +0100
    10.3 @@ -34,10 +34,10 @@
    10.4  
    10.5  val _ = Theory.setup
    10.6   (ML_Antiquotation.value @{binding source}
    10.7 -    (Scan.lift Args.text_source_position >> (fn {delimited, text, pos} =>
    10.8 +    (Scan.lift Args.text_source_position >> (fn {delimited, text, range} =>
    10.9        "{delimited = " ^ Bool.toString delimited ^
   10.10        ", text = " ^ ML_Syntax.print_string text ^
   10.11 -      ", pos = " ^ ML_Syntax.print_position pos ^ "}")));
   10.12 +      ", range = " ^ ML_Syntax.print_range range ^ "}")));
   10.13  
   10.14  
   10.15  (* formal entities *)
    11.1 --- a/src/Pure/ML/ml_context.ML	Tue Nov 11 15:55:31 2014 +0100
    11.2 +++ b/src/Pure/ML/ml_context.ML	Tue Nov 11 18:16:25 2014 +0100
    11.3 @@ -25,8 +25,8 @@
    11.4    val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
    11.5      ML_Lex.token Antiquote.antiquote list -> unit
    11.6    val eval_source_in: Proof.context option -> ML_Compiler.flags -> Symbol_Pos.source -> unit
    11.7 -  val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
    11.8 -    Context.generic -> Context.generic
    11.9 +  val expression: Position.range -> string -> string ->
   11.10 +    ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
   11.11  end
   11.12  
   11.13  structure ML_Context: ML_CONTEXT =
   11.14 @@ -173,7 +173,7 @@
   11.15    in eval flags pos (ML_Lex.read pos (File.read path)) end;
   11.16  
   11.17  fun eval_source flags source =
   11.18 -  eval flags (#pos source) (ML_Lex.read_source (#SML flags) source);
   11.19 +  eval flags (#1 (#range source)) (ML_Lex.read_source (#SML flags) source);
   11.20  
   11.21  fun eval_in ctxt flags pos ants =
   11.22    Context.setmp_thread_data (Option.map Context.Proof ctxt)
   11.23 @@ -183,11 +183,12 @@
   11.24    Context.setmp_thread_data (Option.map Context.Proof ctxt)
   11.25      (fn () => eval_source flags source) ();
   11.26  
   11.27 -fun expression pos bind body ants =
   11.28 +fun expression range bind body ants =
   11.29    exec (fn () =>
   11.30 -    eval ML_Compiler.flags pos
   11.31 -     (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
   11.32 -      ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
   11.33 +    eval ML_Compiler.flags (#1 range)
   11.34 +     (ML_Lex.read_set_range range ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @
   11.35 +      ants @
   11.36 +      ML_Lex.read_set_range range (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
   11.37  
   11.38  end;
   11.39  
    12.1 --- a/src/Pure/ML/ml_file.ML	Tue Nov 11 15:55:31 2014 +0100
    12.2 +++ b/src/Pure/ML/ml_file.ML	Tue Nov 11 18:16:25 2014 +0100
    12.3 @@ -13,7 +13,7 @@
    12.4          let
    12.5            val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
    12.6            val provide = Resources.provide (src_path, digest);
    12.7 -          val source = {delimited = true, text = cat_lines lines, pos = pos};
    12.8 +          val source = {delimited = true, text = cat_lines lines, range = (pos, pos)};
    12.9            val flags = {SML = false, exchange = false, redirect = true, verbose = true};
   12.10          in
   12.11            gthy
    13.1 --- a/src/Pure/ML/ml_lex.ML	Tue Nov 11 15:55:31 2014 +0100
    13.2 +++ b/src/Pure/ML/ml_lex.ML	Tue Nov 11 18:16:25 2014 +0100
    13.3 @@ -26,6 +26,7 @@
    13.4        Source.source) Source.source
    13.5    val tokenize: string -> token list
    13.6    val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
    13.7 +  val read_set_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list
    13.8    val read_source: bool -> Symbol_Pos.source -> token Antiquote.antiquote list
    13.9  end;
   13.10  
   13.11 @@ -325,7 +326,11 @@
   13.12  
   13.13  val read = gen_read false;
   13.14  
   13.15 -fun read_source SML {delimited, text, pos} =
   13.16 +fun read_set_range range =
   13.17 +  read Position.none
   13.18 +  #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq);
   13.19 +
   13.20 +fun read_source SML ({delimited, text, range = (pos, _)}: Symbol_Pos.source) =
   13.21    let
   13.22      val language = if SML then Markup.language_SML else Markup.language_ML;
   13.23      val _ =
    14.1 --- a/src/Pure/ML/ml_syntax.ML	Tue Nov 11 15:55:31 2014 +0100
    14.2 +++ b/src/Pure/ML/ml_syntax.ML	Tue Nov 11 18:16:25 2014 +0100
    14.3 @@ -20,6 +20,7 @@
    14.4    val print_strings: string list -> string
    14.5    val print_properties: Properties.T -> string
    14.6    val print_position: Position.T -> string
    14.7 +  val print_range: Position.range -> string
    14.8    val make_binding: string * Position.T -> string
    14.9    val print_indexname: indexname -> string
   14.10    val print_class: class -> string
   14.11 @@ -77,8 +78,15 @@
   14.12  val print_strings = print_list print_string;
   14.13  
   14.14  val print_properties = print_list (print_pair print_string print_string);
   14.15 -fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
   14.16 -fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos);
   14.17 +
   14.18 +fun print_position pos =
   14.19 +  "Position.of_properties " ^ print_properties (Position.properties_of pos);
   14.20 +
   14.21 +fun print_range range =
   14.22 +  "Position.range_of_properties " ^ print_properties (Position.properties_of_range range);
   14.23 +
   14.24 +fun make_binding (name, pos) =
   14.25 +  "Binding.make " ^ print_pair print_string print_position (name, pos);
   14.26  
   14.27  val print_indexname = print_pair print_string print_int;
   14.28  
    15.1 --- a/src/Pure/PIDE/markup.ML	Tue Nov 11 15:55:31 2014 +0100
    15.2 +++ b/src/Pure/PIDE/markup.ML	Tue Nov 11 18:16:25 2014 +0100
    15.3 @@ -47,6 +47,7 @@
    15.4    val completionN: string val completion: T
    15.5    val no_completionN: string val no_completion: T
    15.6    val lineN: string
    15.7 +  val end_lineN: string
    15.8    val offsetN: string
    15.9    val end_offsetN: string
   15.10    val fileN: string
   15.11 @@ -329,8 +330,11 @@
   15.12  (* position *)
   15.13  
   15.14  val lineN = "line";
   15.15 +val end_lineN = "end_line";
   15.16 +
   15.17  val offsetN = "offset";
   15.18  val end_offsetN = "end_offset";
   15.19 +
   15.20  val fileN = "file";
   15.21  val idN = "id";
   15.22  
    16.1 --- a/src/Pure/PIDE/markup.scala	Tue Nov 11 15:55:31 2014 +0100
    16.2 +++ b/src/Pure/PIDE/markup.scala	Tue Nov 11 18:16:25 2014 +0100
    16.3 @@ -100,6 +100,7 @@
    16.4    /* position */
    16.5  
    16.6    val LINE = "line"
    16.7 +  val END_LINE = "line"
    16.8    val OFFSET = "offset"
    16.9    val END_OFFSET = "end_offset"
   16.10    val FILE = "file"
    17.1 --- a/src/Pure/Syntax/syntax.ML	Tue Nov 11 15:55:31 2014 +0100
    17.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Nov 11 18:16:25 2014 +0100
    17.3 @@ -163,21 +163,21 @@
    17.4  
    17.5  local
    17.6  
    17.7 -fun token_position (XML.Elem ((name, props), _)) =
    17.8 +fun token_range (XML.Elem ((name, props), _)) =
    17.9        if name = Markup.tokenN
   17.10 -      then (Markup.is_delimited props, Position.of_properties props)
   17.11 -      else (false, Position.none)
   17.12 -  | token_position (XML.Text _) = (false, Position.none);
   17.13 +      then (Markup.is_delimited props, Position.range_of_properties props)
   17.14 +      else (false, Position.no_range)
   17.15 +  | token_range (XML.Text _) = (false, Position.no_range);
   17.16  
   17.17 -fun token_source tree =
   17.18 +fun token_source tree : Symbol_Pos.source =
   17.19    let
   17.20      val text = XML.content_of [tree];
   17.21 -    val (delimited, pos) = token_position tree;
   17.22 -  in {delimited = delimited, text = text, pos = pos} end;
   17.23 +    val (delimited, range) = token_range tree;
   17.24 +  in {delimited = delimited, text = text, range = range} end;
   17.25  
   17.26  in
   17.27  
   17.28 -fun read_token_pos str = #2 (token_position (YXML.parse str handle Fail msg => error msg));
   17.29 +fun read_token_pos str = #1 (#2 (token_range (YXML.parse str handle Fail msg => error msg)));
   17.30  
   17.31  fun read_token str = token_source (YXML.parse str handle Fail msg => error msg);
   17.32  
   17.33 @@ -187,8 +187,9 @@
   17.34        let
   17.35          val source = token_source tree;
   17.36          val syms = Symbol_Pos.source_explode source;
   17.37 -        val _ = Context_Position.report ctxt (#pos source) (markup (#delimited source));
   17.38 -      in parse (syms, #pos source) end;
   17.39 +        val (pos, _) = #range source;
   17.40 +        val _ = Context_Position.report ctxt pos (markup (#delimited source));
   17.41 +      in parse (syms, pos) end;
   17.42    in
   17.43      (case YXML.parse_body str handle Fail msg => error msg of
   17.44        body as [tree as XML.Elem ((name, _), _)] =>
    18.1 --- a/src/Pure/Syntax/syntax_phases.ML	Tue Nov 11 15:55:31 2014 +0100
    18.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Tue Nov 11 18:16:25 2014 +0100
    18.3 @@ -462,10 +462,11 @@
    18.4        | decode ps (Ast.Appl asts) = decode_appl ps asts;
    18.5  
    18.6      val source = Syntax.read_token str;
    18.7 +    val (pos, _) = #range source;
    18.8      val syms = Symbol_Pos.source_explode source;
    18.9      val ast =
   18.10 -      parse_asts ctxt true root (syms, #pos source)
   18.11 -      |> uncurry (report_result ctxt (#pos source))
   18.12 +      parse_asts ctxt true root (syms, pos)
   18.13 +      |> uncurry (report_result ctxt pos)
   18.14        |> decode [];
   18.15      val _ = Context_Position.reports_text ctxt (! reports);
   18.16    in ast end;
    19.1 --- a/src/Pure/Thy/latex.ML	Tue Nov 11 15:55:31 2014 +0100
    19.2 +++ b/src/Pure/Thy/latex.ML	Tue Nov 11 18:16:25 2014 +0100
    19.3 @@ -132,7 +132,7 @@
    19.4        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
    19.5      else if Token.is_kind Token.Verbatim tok then
    19.6        let
    19.7 -        val {text, pos, ...} = Token.source_position_of tok;
    19.8 +        val {text, range = (pos, _), ...} = Token.source_position_of tok;
    19.9          val ants = Antiquote.read (Symbol_Pos.explode (text, pos), pos);
   19.10          val out = implode (map output_syms_antiq ants);
   19.11        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
    20.1 --- a/src/Pure/Thy/thy_output.ML	Tue Nov 11 15:55:31 2014 +0100
    20.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Nov 11 18:16:25 2014 +0100
    20.3 @@ -195,10 +195,10 @@
    20.4      val _ = Position.reports (maps words ants);
    20.5    in implode (map expand ants) end;
    20.6  
    20.7 -fun check_text {delimited, text, pos} state =
    20.8 - (Position.report pos (Markup.language_document delimited);
    20.9 +fun check_text {delimited, text, range} state =
   20.10 + (Position.report (fst range) (Markup.language_document delimited);
   20.11    if Toplevel.is_skipped_proof state then ()
   20.12 -  else ignore (eval_antiquote state (text, pos)));
   20.13 +  else ignore (eval_antiquote state (text, fst range)));
   20.14  
   20.15  
   20.16  
   20.17 @@ -372,7 +372,7 @@
   20.18          Parse.position (Scan.one (Token.is_command andf is_markup mark o Token.content_of)) --
   20.19        Scan.repeat tag --
   20.20        Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
   20.21 -      >> (fn (((tok, pos'), tags), {text, pos, ...}) =>
   20.22 +      >> (fn (((tok, pos'), tags), {text, range = (pos, _), ...}) =>
   20.23          let val name = Token.content_of tok
   20.24          in (SOME (name, pos', tags), (mk (name, (text, pos)), (flag, d))) end));
   20.25  
   20.26 @@ -385,7 +385,7 @@
   20.27  
   20.28      val cmt = Scan.peek (fn d =>
   20.29        Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source)
   20.30 -      >> (fn {text, pos, ...} => (NONE, (MarkupToken ("cmt", (text, pos)), ("", d)))));
   20.31 +      >> (fn {text, range = (pos, _), ...} => (NONE, (MarkupToken ("cmt", (text, pos)), ("", d)))));
   20.32  
   20.33      val other = Scan.peek (fn d =>
   20.34         Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
   20.35 @@ -482,7 +482,7 @@
   20.36  
   20.37  fun pretty_text_report ctxt source =
   20.38    let
   20.39 -    val {delimited, pos, ...} = source;
   20.40 +    val {delimited, range = (pos, _), ...} = source;
   20.41      val _ = Context_Position.report ctxt pos (Markup.language_text delimited);
   20.42      val (s, _) = Symbol_Pos.source_content source;
   20.43    in pretty_text ctxt s end;
   20.44 @@ -664,7 +664,7 @@
   20.45  
   20.46  fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position)
   20.47    (fn {context = ctxt, ...} => fn source =>
   20.48 -   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source) (ml source);
   20.49 +   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#1 (#range source)) (ml source);
   20.50      Symbol_Pos.source_content source |> #1
   20.51      |> verbatim_text ctxt));
   20.52  
    21.1 --- a/src/Pure/Thy/thy_syntax.ML	Tue Nov 11 15:55:31 2014 +0100
    21.2 +++ b/src/Pure/Thy/thy_syntax.ML	Tue Nov 11 18:16:25 2014 +0100
    21.3 @@ -26,7 +26,7 @@
    21.4  
    21.5  fun reports_of_token tok =
    21.6    let
    21.7 -    val {text, pos, ...} = Token.source_position_of tok;
    21.8 +    val {text, range = (pos, _), ...} = Token.source_position_of tok;
    21.9      val malformed_symbols =
   21.10        Symbol_Pos.explode (text, pos)
   21.11        |> map_filter (fn (sym, pos) =>
    22.1 --- a/src/Pure/Tools/rail.ML	Tue Nov 11 15:55:31 2014 +0100
    22.2 +++ b/src/Pure/Tools/rail.ML	Tue Nov 11 18:16:25 2014 +0100
    22.3 @@ -283,7 +283,7 @@
    22.4  
    22.5  fun read ctxt (source: Symbol_Pos.source) =
    22.6    let
    22.7 -    val {text, pos, ...} = source;
    22.8 +    val {text, range = (pos, _), ...} = source;
    22.9      val _ = Context_Position.report ctxt pos Markup.language_rail;
   22.10      val toks = tokenize (Symbol_Pos.explode (text, pos));
   22.11      val _ = Context_Position.reports ctxt (maps reports_of_token toks);