more abstract type Input.source;
authorwenzelm
Sun Nov 30 12:24:56 2014 +0100 (2014-11-30)
changeset 59064a8bcb5a446c8
parent 59063 b3c45d0e4fe1
child 59065 8ce02aafc363
more abstract type Input.source;
src/Doc/antiquote_setup.ML
src/HOL/ex/Cartouche_Examples.thy
src/Pure/General/input.ML
src/Pure/General/symbol_pos.ML
src/Pure/Isar/args.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/parse.ML
src/Pure/Isar/proof_context.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/ROOT
src/Pure/ROOT.ML
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	Sat Nov 29 14:43:10 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sun Nov 30 12:24:56 2014 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4    | _ => error ("Single ML name expected in input: " ^ quote txt));
     1.5  
     1.6  fun prep_ml source =
     1.7 -  (#1 (Symbol_Pos.source_content source), ML_Lex.read_source false source);
     1.8 +  (#1 (Input.source_content source), ML_Lex.read_source false source);
     1.9  
    1.10  fun index_ml name kind ml = Thy_Output.antiquotation name
    1.11    (Scan.lift (Args.text_source_position -- Scan.option (Args.colon |-- Args.text_source_position)))
    1.12 @@ -90,7 +90,7 @@
    1.13          else txt1 ^ " : " ^ txt2;
    1.14        val txt' = if kind = "" then txt else kind ^ " " ^ txt;
    1.15  
    1.16 -      val (pos, _) = #range source1;
    1.17 +      val pos = Input.pos_of source1;
    1.18        val _ =
    1.19          ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2))
    1.20            handle ERROR msg => error (msg ^ Position.here pos);
     2.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Sat Nov 29 14:43:10 2014 +0100
     2.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Sun Nov 30 12:24:56 2014 +0100
     2.3 @@ -146,8 +146,7 @@
     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 (pos, _) = #range source;
     2.8 -        val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags pos toks;
     2.9 +        val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks;
    2.10        in "" end);
    2.11  *}
    2.12  
    2.13 @@ -204,7 +203,7 @@
    2.14  structure ML_Tactic:
    2.15  sig
    2.16    val set: (Proof.context -> tactic) -> Proof.context -> Proof.context
    2.17 -  val ml_tactic: Symbol_Pos.source -> Proof.context -> tactic
    2.18 +  val ml_tactic: Input.source -> Proof.context -> tactic
    2.19  end =
    2.20  struct
    2.21    structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac);
    2.22 @@ -214,7 +213,7 @@
    2.23    fun ml_tactic source ctxt =
    2.24      let
    2.25        val ctxt' = ctxt |> Context.proof_map
    2.26 -        (ML_Context.expression (#range source) "tactic" "Proof.context -> tactic"
    2.27 +        (ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic"
    2.28            "Context.map_proof (ML_Tactic.set tactic)"
    2.29            (ML_Lex.read Position.none "fn ctxt: Proof.context =>" @
    2.30             ML_Lex.read_source false source));
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/General/input.ML	Sun Nov 30 12:24:56 2014 +0100
     3.3 @@ -0,0 +1,43 @@
     3.4 +(*  Title:      Pure/General/input.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Generic input with position information.
     3.8 +*)
     3.9 +
    3.10 +signature INPUT =
    3.11 +sig
    3.12 +  type source
    3.13 +  val is_delimited: source -> bool
    3.14 +  val text_of: source -> Symbol_Pos.text
    3.15 +  val pos_of: source -> Position.T
    3.16 +  val range_of: source -> Position.range
    3.17 +  val source: bool -> Symbol_Pos.text -> Position.range -> source
    3.18 +  val source_explode: source -> Symbol_Pos.T list
    3.19 +  val source_content: source -> string * Position.T
    3.20 +end;
    3.21 +
    3.22 +structure Input: INPUT =
    3.23 +struct
    3.24 +
    3.25 +abstype source = Source of {delimited: bool, text: Symbol_Pos.text, range: Position.range}
    3.26 +with
    3.27 +
    3.28 +fun is_delimited (Source {delimited, ...}) = delimited;
    3.29 +fun text_of (Source {text, ...}) = text;
    3.30 +fun pos_of (Source {range = (pos, _), ...}) = pos;
    3.31 +fun range_of (Source {range, ...}) = range;
    3.32 +
    3.33 +fun source delimited text range =
    3.34 +  Source {delimited = delimited, text = text, range = range};
    3.35 +
    3.36 +fun source_explode (Source {text, range = (pos, _), ...}) =
    3.37 +  Symbol_Pos.explode (text, pos);
    3.38 +
    3.39 +fun source_content (Source {text, range = (pos, _), ...}) =
    3.40 +  let val syms = Symbol_Pos.explode (text, pos)
    3.41 +  in (Symbol_Pos.content syms, pos) end;
    3.42 +
    3.43 +end;
    3.44 +
    3.45 +end;
    3.46 +
     4.1 --- a/src/Pure/General/symbol_pos.ML	Sat Nov 29 14:43:10 2014 +0100
     4.2 +++ b/src/Pure/General/symbol_pos.ML	Sun Nov 30 12:24:56 2014 +0100
     4.3 @@ -39,9 +39,6 @@
     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, range: Position.range}
     4.8 -  val source_explode: source -> T list
     4.9 -  val source_content: source -> string * Position.T
    4.10    val scan_ident: T list -> T list * T list
    4.11    val is_identifier: string -> bool
    4.12  end;
    4.13 @@ -253,16 +250,6 @@
    4.14    in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
    4.15  
    4.16  
    4.17 -(* full source information *)
    4.18 -
    4.19 -type source = {delimited: bool, text: text, range: Position.range};
    4.20 -
    4.21 -fun source_explode {delimited = _, text, range = (pos, _)} = explode (text, pos);
    4.22 -
    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 -
    4.27  (* identifiers *)
    4.28  
    4.29  local
     5.1 --- a/src/Pure/Isar/args.ML	Sat Nov 29 14:43:10 2014 +0100
     5.2 +++ b/src/Pure/Isar/args.ML	Sun Nov 30 12:24:56 2014 +0100
     5.3 @@ -22,11 +22,11 @@
     5.4    val mode: string -> bool parser
     5.5    val maybe: 'a parser -> 'a option parser
     5.6    val cartouche_inner_syntax: string parser
     5.7 -  val cartouche_source_position: Symbol_Pos.source parser
     5.8 -  val text_source_position: Symbol_Pos.source parser
     5.9 +  val cartouche_source_position: Input.source parser
    5.10 +  val text_source_position: Input.source parser
    5.11    val text: string parser
    5.12    val name_inner_syntax: string parser
    5.13 -  val name_source_position: Symbol_Pos.source parser
    5.14 +  val name_source_position: Input.source parser
    5.15    val name: string parser
    5.16    val binding: binding parser
    5.17    val alt_name: string parser
    5.18 @@ -46,7 +46,7 @@
    5.19    val named_fact: (string -> string option * thm list) -> thm list parser
    5.20    val named_attribute: (string * Position.T -> morphism -> attribute) ->
    5.21      (morphism -> attribute) parser
    5.22 -  val text_declaration: (Symbol_Pos.source -> declaration) -> declaration parser
    5.23 +  val text_declaration: (Input.source -> declaration) -> declaration parser
    5.24    val typ_abbrev: typ context_parser
    5.25    val typ: typ context_parser
    5.26    val term: term context_parser
     6.1 --- a/src/Pure/Isar/attrib.ML	Sat Nov 29 14:43:10 2014 +0100
     6.2 +++ b/src/Pure/Isar/attrib.ML	Sun Nov 30 12:24:56 2014 +0100
     6.3 @@ -41,7 +41,7 @@
     6.4    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
     6.5    val local_setup: Binding.binding -> attribute context_parser -> string ->
     6.6      local_theory -> local_theory
     6.7 -  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
     6.8 +  val attribute_setup: bstring * Position.T -> Input.source -> string ->
     6.9      local_theory -> local_theory
    6.10    val internal: (morphism -> attribute) -> Token.src
    6.11    val add_del: attribute -> attribute -> attribute context_parser
    6.12 @@ -49,7 +49,7 @@
    6.13    val thms: thm list context_parser
    6.14    val multi_thm: thm list context_parser
    6.15    val check_attribs: Proof.context -> Token.src list -> Token.src list
    6.16 -  val read_attribs: Proof.context -> Symbol_Pos.source -> Token.src list
    6.17 +  val read_attribs: Proof.context -> Input.source -> Token.src list
    6.18    val transform_facts: morphism ->
    6.19      (Attrib.binding * (thm list * Token.src list) list) list ->
    6.20      (Attrib.binding * (thm list * Token.src list) list) list
    6.21 @@ -208,7 +208,7 @@
    6.22  
    6.23  fun attribute_setup name source comment =
    6.24    ML_Lex.read_source false source
    6.25 -  |> ML_Context.expression (#range source) "parser" "Thm.attribute context_parser"
    6.26 +  |> ML_Context.expression (Input.range_of source) "parser" "Thm.attribute context_parser"
    6.27      ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
    6.28        " parser " ^ ML_Syntax.print_string comment ^ ")")
    6.29    |> Context.proof_map;
    6.30 @@ -287,11 +287,11 @@
    6.31  fun read_attribs ctxt source =
    6.32    let
    6.33      val keywords = Thy_Header.get_keywords' ctxt;
    6.34 -    val syms = Symbol_Pos.source_explode source;
    6.35 +    val syms = Input.source_explode source;
    6.36    in
    6.37      (case Token.read_no_commands keywords Parse.attribs syms of
    6.38        [raw_srcs] => check_attribs ctxt raw_srcs
    6.39 -    | _ => error ("Malformed attributes" ^ Position.here (#1 (#range source))))
    6.40 +    | _ => error ("Malformed attributes" ^ Position.here (Input.pos_of source)))
    6.41    end;
    6.42  
    6.43  
     7.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 29 14:43:10 2014 +0100
     7.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 30 12:24:56 2014 +0100
     7.3 @@ -6,20 +6,19 @@
     7.4  
     7.5  signature ISAR_CMD =
     7.6  sig
     7.7 -  val global_setup: Symbol_Pos.source -> theory -> theory
     7.8 -  val local_setup: Symbol_Pos.source -> Proof.context -> Proof.context
     7.9 -  val parse_ast_translation: Symbol_Pos.source -> theory -> theory
    7.10 -  val parse_translation: Symbol_Pos.source -> theory -> theory
    7.11 -  val print_translation: Symbol_Pos.source -> theory -> theory
    7.12 -  val typed_print_translation: Symbol_Pos.source -> theory -> theory
    7.13 -  val print_ast_translation: Symbol_Pos.source -> theory -> theory
    7.14 +  val global_setup: Input.source -> theory -> theory
    7.15 +  val local_setup: Input.source -> Proof.context -> Proof.context
    7.16 +  val parse_ast_translation: Input.source -> theory -> theory
    7.17 +  val parse_translation: Input.source -> theory -> theory
    7.18 +  val print_translation: Input.source -> theory -> theory
    7.19 +  val typed_print_translation: Input.source -> theory -> theory
    7.20 +  val print_ast_translation: Input.source -> theory -> theory
    7.21    val translations: (xstring * string) Syntax.trrule list -> theory -> theory
    7.22    val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
    7.23 -  val oracle: bstring * Position.range -> Symbol_Pos.source -> theory -> theory
    7.24 +  val oracle: bstring * Position.range -> Input.source -> theory -> theory
    7.25    val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
    7.26 -  val declaration: {syntax: bool, pervasive: bool} ->
    7.27 -    Symbol_Pos.source -> local_theory -> local_theory
    7.28 -  val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
    7.29 +  val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
    7.30 +  val simproc_setup: string * Position.T -> string list -> Input.source ->
    7.31      string list -> local_theory -> local_theory
    7.32    val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    7.33    val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    7.34 @@ -32,7 +31,7 @@
    7.35    val immediate_proof: Toplevel.transition -> Toplevel.transition
    7.36    val done_proof: Toplevel.transition -> Toplevel.transition
    7.37    val skip_proof: Toplevel.transition -> Toplevel.transition
    7.38 -  val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
    7.39 +  val ml_diag: bool -> Input.source -> Toplevel.transition -> Toplevel.transition
    7.40    val diag_state: Proof.context -> Toplevel.state
    7.41    val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
    7.42    val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
    7.43 @@ -60,13 +59,13 @@
    7.44  
    7.45  fun global_setup source =
    7.46    ML_Lex.read_source false source
    7.47 -  |> ML_Context.expression (#range source) "setup" "theory -> theory"
    7.48 +  |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
    7.49      "Context.map_theory setup"
    7.50    |> Context.theory_map;
    7.51  
    7.52  fun local_setup source =
    7.53    ML_Lex.read_source false source
    7.54 -  |> ML_Context.expression (#range source) "local_setup" "local_theory -> local_theory"
    7.55 +  |> ML_Context.expression (Input.range_of source) "local_setup" "local_theory -> local_theory"
    7.56      "Context.map_proof local_setup"
    7.57    |> Context.proof_map;
    7.58  
    7.59 @@ -75,35 +74,35 @@
    7.60  
    7.61  fun parse_ast_translation source =
    7.62    ML_Lex.read_source false source
    7.63 -  |> ML_Context.expression (#range source) "parse_ast_translation"
    7.64 +  |> ML_Context.expression (Input.range_of source) "parse_ast_translation"
    7.65      "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    7.66      "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    7.67    |> Context.theory_map;
    7.68  
    7.69  fun parse_translation source =
    7.70    ML_Lex.read_source false source
    7.71 -  |> ML_Context.expression (#range source) "parse_translation"
    7.72 +  |> ML_Context.expression (Input.range_of source) "parse_translation"
    7.73      "(string * (Proof.context -> term list -> term)) list"
    7.74      "Context.map_theory (Sign.parse_translation parse_translation)"
    7.75    |> Context.theory_map;
    7.76  
    7.77  fun print_translation source =
    7.78    ML_Lex.read_source false source
    7.79 -  |> ML_Context.expression (#range source) "print_translation"
    7.80 +  |> ML_Context.expression (Input.range_of source) "print_translation"
    7.81      "(string * (Proof.context -> term list -> term)) list"
    7.82      "Context.map_theory (Sign.print_translation print_translation)"
    7.83    |> Context.theory_map;
    7.84  
    7.85  fun typed_print_translation source =
    7.86    ML_Lex.read_source false source
    7.87 -  |> ML_Context.expression (#range source) "typed_print_translation"
    7.88 +  |> ML_Context.expression (Input.range_of source) "typed_print_translation"
    7.89      "(string * (Proof.context -> typ -> term list -> term)) list"
    7.90      "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
    7.91    |> Context.theory_map;
    7.92  
    7.93  fun print_ast_translation source =
    7.94    ML_Lex.read_source false source
    7.95 -  |> ML_Context.expression (#range source) "print_ast_translation"
    7.96 +  |> ML_Context.expression (Input.range_of source) "print_ast_translation"
    7.97      "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    7.98      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
    7.99    |> Context.theory_map;
   7.100 @@ -129,7 +128,7 @@
   7.101  
   7.102  fun oracle (name, range) source =
   7.103    let
   7.104 -    val body_range = #range source;
   7.105 +    val body_range = Input.range_of source;
   7.106      val body = ML_Lex.read_source false source;
   7.107  
   7.108      val hidden = ML_Lex.read Position.none;
   7.109 @@ -164,7 +163,7 @@
   7.110  
   7.111  fun declaration {syntax, pervasive} source =
   7.112    ML_Lex.read_source false source
   7.113 -  |> ML_Context.expression (#range source) "declaration" "Morphism.declaration"
   7.114 +  |> ML_Context.expression (Input.range_of source) "declaration" "Morphism.declaration"
   7.115      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
   7.116        \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
   7.117    |> Context.proof_map;
   7.118 @@ -174,7 +173,7 @@
   7.119  
   7.120  fun simproc_setup name lhss source identifier =
   7.121    ML_Lex.read_source false source
   7.122 -  |> ML_Context.expression (#range source) "proc"
   7.123 +  |> ML_Context.expression (Input.range_of source) "proc"
   7.124      "Morphism.morphism -> Proof.context -> cterm -> thm option"
   7.125      ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
   7.126        \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
     8.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Nov 29 14:43:10 2014 +0100
     8.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 30 12:24:56 2014 +0100
     8.3 @@ -208,7 +208,7 @@
     8.4      (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
     8.5          let
     8.6            val ([{lines, pos, ...}], thy') = files thy;
     8.7 -          val source = {delimited = true, text = cat_lines lines, range = (pos, pos)};
     8.8 +          val source = Input.source true (cat_lines lines) (pos, pos);
     8.9            val flags = {SML = true, exchange = false, redirect = true, verbose = true};
    8.10          in
    8.11            thy' |> Context.theory_map
     9.1 --- a/src/Pure/Isar/method.ML	Sat Nov 29 14:43:10 2014 +0100
     9.2 +++ b/src/Pure/Isar/method.ML	Sun Nov 30 12:24:56 2014 +0100
     9.3 @@ -61,8 +61,7 @@
     9.4    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
     9.5    val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
     9.6      local_theory -> local_theory
     9.7 -  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
     9.8 -    local_theory -> local_theory
     9.9 +  val method_setup: bstring * Position.T -> Input.source -> string -> local_theory -> local_theory
    9.10    val method: Proof.context -> Token.src -> Proof.context -> method
    9.11    val method_closure: Proof.context -> Token.src -> Token.src
    9.12    val method_cmd: Proof.context -> Token.src -> Proof.context -> method
    9.13 @@ -282,7 +281,7 @@
    9.14      Scan.lift (Args.text_declaration (fn source =>
    9.15        let
    9.16          val context' = context |>
    9.17 -          ML_Context.expression (#range source)
    9.18 +          ML_Context.expression (Input.range_of source)
    9.19              "tactic" "Morphism.morphism -> thm list -> tactic"
    9.20              "Method.set_tactic tactic"
    9.21              (ML_Lex.read Position.none "fn morphism: Morphism.morphism => fn facts: thm list =>" @
    9.22 @@ -381,7 +380,7 @@
    9.23  
    9.24  fun method_setup name source comment =
    9.25    ML_Lex.read_source false source
    9.26 -  |> ML_Context.expression (#range source) "parser"
    9.27 +  |> ML_Context.expression (Input.range_of source) "parser"
    9.28      "(Proof.context -> Proof.method) context_parser"
    9.29      ("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
    9.30        " parser " ^ ML_Syntax.print_string comment ^ ")")
    10.1 --- a/src/Pure/Isar/parse.ML	Sat Nov 29 14:43:10 2014 +0100
    10.2 +++ b/src/Pure/Isar/parse.ML	Sun Nov 30 12:24:56 2014 +0100
    10.3 @@ -16,7 +16,7 @@
    10.4    val token: 'a parser -> Token.T parser
    10.5    val range: 'a parser -> ('a * Position.range) parser
    10.6    val position: 'a parser -> ('a * Position.T) parser
    10.7 -  val source_position: 'a parser -> Symbol_Pos.source parser
    10.8 +  val source_position: 'a parser -> Input.source parser
    10.9    val inner_syntax: 'a parser -> string parser
   10.10    val command_: string parser
   10.11    val keyword: string parser
   10.12 @@ -92,8 +92,8 @@
   10.13    val simple_fixes: (binding * string option) list parser
   10.14    val fixes: (binding * string option * mixfix) list parser
   10.15    val for_fixes: (binding * string option * mixfix) list parser
   10.16 -  val ML_source: Symbol_Pos.source parser
   10.17 -  val document_source: Symbol_Pos.source parser
   10.18 +  val ML_source: Input.source parser
   10.19 +  val document_source: Input.source parser
   10.20    val term_group: string parser
   10.21    val prop_group: string parser
   10.22    val term: string parser
    11.1 --- a/src/Pure/Isar/proof_context.ML	Sat Nov 29 14:43:10 2014 +0100
    11.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Nov 30 12:24:56 2014 +0100
    11.3 @@ -403,7 +403,7 @@
    11.4  
    11.5  fun read_class ctxt text =
    11.6    let
    11.7 -    val (c, reports) = check_class ctxt (Symbol_Pos.source_content (Syntax.read_token text));
    11.8 +    val (c, reports) = check_class ctxt (Input.source_content (Syntax.read_token text));
    11.9      val _ = Position.reports reports;
   11.10    in c end;
   11.11  
   11.12 @@ -471,7 +471,7 @@
   11.13  fun read_type_name ctxt flags text =
   11.14    let
   11.15      val (T, reports) =
   11.16 -      check_type_name ctxt flags (Symbol_Pos.source_content (Syntax.read_token text));
   11.17 +      check_type_name ctxt flags (Input.source_content (Syntax.read_token text));
   11.18      val _ = Position.reports reports;
   11.19    in T end;
   11.20  
   11.21 @@ -519,7 +519,7 @@
   11.22  
   11.23  fun read_const ctxt flags text =
   11.24    let
   11.25 -    val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
   11.26 +    val (xname, pos) = Input.source_content (Syntax.read_token text);
   11.27      val (t, reports) = check_const ctxt flags (xname, [pos]);
   11.28      val _ = Position.reports reports;
   11.29    in t end;
    12.1 --- a/src/Pure/Isar/token.ML	Sat Nov 29 14:43:10 2014 +0100
    12.2 +++ b/src/Pure/Isar/token.ML	Sun Nov 30 12:24:56 2014 +0100
    12.3 @@ -52,7 +52,7 @@
    12.4    val is_blank: T -> bool
    12.5    val is_newline: T -> bool
    12.6    val inner_syntax_of: T -> string
    12.7 -  val source_position_of: T -> Symbol_Pos.source
    12.8 +  val source_position_of: T -> Input.source
    12.9    val content_of: T -> string
   12.10    val keyword_markup: bool * Markup.T -> string -> Markup.T
   12.11    val completion_report: T -> Position.report_text list
   12.12 @@ -269,7 +269,7 @@
   12.13      in YXML.string_of tree end;
   12.14  
   12.15  fun source_position_of (Token ((source, range), (kind, _), _)) =
   12.16 -  {delimited = delimited_kind kind, text = source, range = range};
   12.17 +  Input.source (delimited_kind kind) source range;
   12.18  
   12.19  fun content_of (Token (_, (_, x), _)) = x;
   12.20  
    13.1 --- a/src/Pure/ML/ml_antiquotations.ML	Sat Nov 29 14:43:10 2014 +0100
    13.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Sun Nov 30 12:24:56 2014 +0100
    13.3 @@ -34,10 +34,10 @@
    13.4  
    13.5  val _ = Theory.setup
    13.6   (ML_Antiquotation.value @{binding source}
    13.7 -    (Scan.lift Args.text_source_position >> (fn {delimited, text, range} =>
    13.8 -      "{delimited = " ^ Bool.toString delimited ^
    13.9 -      ", text = " ^ ML_Syntax.print_string text ^
   13.10 -      ", range = " ^ ML_Syntax.print_range range ^ "}")));
   13.11 +    (Scan.lift Args.text_source_position >> (fn source =>
   13.12 +      "Input.source " ^ Bool.toString (Input.is_delimited source) ^ " " ^
   13.13 +        ML_Syntax.print_string (Input.text_of source) ^ " " ^
   13.14 +        ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
   13.15  
   13.16  
   13.17  (* formal entities *)
    14.1 --- a/src/Pure/ML/ml_context.ML	Sat Nov 29 14:43:10 2014 +0100
    14.2 +++ b/src/Pure/ML/ml_context.ML	Sun Nov 30 12:24:56 2014 +0100
    14.3 @@ -21,10 +21,10 @@
    14.4      Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
    14.5    val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
    14.6    val eval_file: ML_Compiler.flags -> Path.T -> unit
    14.7 -  val eval_source: ML_Compiler.flags -> Symbol_Pos.source -> unit
    14.8 +  val eval_source: ML_Compiler.flags -> Input.source -> unit
    14.9    val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
   14.10      ML_Lex.token Antiquote.antiquote list -> unit
   14.11 -  val eval_source_in: Proof.context option -> ML_Compiler.flags -> Symbol_Pos.source -> unit
   14.12 +  val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit
   14.13    val expression: Position.range -> string -> string -> string ->
   14.14      ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
   14.15  end
   14.16 @@ -173,7 +173,7 @@
   14.17    in eval flags pos (ML_Lex.read pos (File.read path)) end;
   14.18  
   14.19  fun eval_source flags source =
   14.20 -  eval flags (#1 (#range source)) (ML_Lex.read_source (#SML flags) source);
   14.21 +  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
   14.22  
   14.23  fun eval_in ctxt flags pos ants =
   14.24    Context.setmp_thread_data (Option.map Context.Proof ctxt)
    15.1 --- a/src/Pure/ML/ml_file.ML	Sat Nov 29 14:43:10 2014 +0100
    15.2 +++ b/src/Pure/ML/ml_file.ML	Sun Nov 30 12:24:56 2014 +0100
    15.3 @@ -13,7 +13,7 @@
    15.4          let
    15.5            val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
    15.6            val provide = Resources.provide (src_path, digest);
    15.7 -          val source = {delimited = true, text = cat_lines lines, range = (pos, pos)};
    15.8 +          val source = Input.source true (cat_lines lines) (pos, pos);
    15.9            val flags = {SML = false, exchange = false, redirect = true, verbose = true};
   15.10          in
   15.11            gthy
    16.1 --- a/src/Pure/ML/ml_lex.ML	Sat Nov 29 14:43:10 2014 +0100
    16.2 +++ b/src/Pure/ML/ml_lex.ML	Sun Nov 30 12:24:56 2014 +0100
    16.3 @@ -27,7 +27,7 @@
    16.4    val tokenize: string -> token list
    16.5    val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
    16.6    val read_set_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list
    16.7 -  val read_source: bool -> Symbol_Pos.source -> token Antiquote.antiquote list
    16.8 +  val read_source: bool -> Input.source -> token Antiquote.antiquote list
    16.9  end;
   16.10  
   16.11  structure ML_Lex: ML_LEX =
   16.12 @@ -330,13 +330,15 @@
   16.13    read Position.none
   16.14    #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq);
   16.15  
   16.16 -fun read_source SML ({delimited, text, range = (pos, _)}: Symbol_Pos.source) =
   16.17 +fun read_source SML source =
   16.18    let
   16.19 +    val pos = Input.pos_of source;
   16.20      val language = if SML then Markup.language_SML else Markup.language_ML;
   16.21      val _ =
   16.22 -      if Position.is_reported_range pos then Position.report pos (language delimited)
   16.23 +      if Position.is_reported_range pos
   16.24 +      then Position.report pos (language (Input.is_delimited source))
   16.25        else ();
   16.26 -  in gen_read SML pos text end;
   16.27 +  in gen_read SML pos (Input.text_of source) end;
   16.28  
   16.29  end;
   16.30  
    17.1 --- a/src/Pure/ROOT	Sat Nov 29 14:43:10 2014 +0100
    17.2 +++ b/src/Pure/ROOT	Sun Nov 30 12:24:56 2014 +0100
    17.3 @@ -81,6 +81,7 @@
    17.4      "General/graph.ML"
    17.5      "General/graph_display.ML"
    17.6      "General/heap.ML"
    17.7 +    "General/input.ML"
    17.8      "General/integer.ML"
    17.9      "General/linear_set.ML"
   17.10      "General/long_name.ML"
    18.1 --- a/src/Pure/ROOT.ML	Sat Nov 29 14:43:10 2014 +0100
    18.2 +++ b/src/Pure/ROOT.ML	Sun Nov 30 12:24:56 2014 +0100
    18.3 @@ -32,6 +32,7 @@
    18.4  use "General/symbol.ML";
    18.5  use "General/position.ML";
    18.6  use "General/symbol_pos.ML";
    18.7 +use "General/input.ML";
    18.8  use "General/antiquote.ML";
    18.9  use "ML/ml_lex.ML";
   18.10  use "ML/ml_parse.ML";
    19.1 --- a/src/Pure/Syntax/syntax.ML	Sat Nov 29 14:43:10 2014 +0100
    19.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Nov 30 12:24:56 2014 +0100
    19.3 @@ -15,7 +15,7 @@
    19.4    val ambiguity_limit_raw: Config.raw
    19.5    val ambiguity_limit: int Config.T
    19.6    val read_token_pos: string -> Position.T
    19.7 -  val read_token: string -> Symbol_Pos.source
    19.8 +  val read_token: string -> Input.source
    19.9    val parse_token: Proof.context -> (XML.tree list -> 'a) ->
   19.10      (bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
   19.11    val parse_sort: Proof.context -> string -> sort
   19.12 @@ -169,11 +169,11 @@
   19.13        else (false, Position.no_range)
   19.14    | token_range (XML.Text _) = (false, Position.no_range);
   19.15  
   19.16 -fun token_source tree : Symbol_Pos.source =
   19.17 +fun token_source tree : Input.source =
   19.18    let
   19.19      val text = XML.content_of [tree];
   19.20      val (delimited, range) = token_range tree;
   19.21 -  in {delimited = delimited, text = text, range = range} end;
   19.22 +  in Input.source delimited text range end;
   19.23  
   19.24  in
   19.25  
   19.26 @@ -186,9 +186,9 @@
   19.27      fun parse_tree tree =
   19.28        let
   19.29          val source = token_source tree;
   19.30 -        val syms = Symbol_Pos.source_explode source;
   19.31 -        val (pos, _) = #range source;
   19.32 -        val _ = Context_Position.report ctxt pos (markup (#delimited source));
   19.33 +        val syms = Input.source_explode source;
   19.34 +        val pos = Input.pos_of source;
   19.35 +        val _ = Context_Position.report ctxt pos (markup (Input.is_delimited source));
   19.36        in parse (syms, pos) end;
   19.37    in
   19.38      (case YXML.parse_body str handle Fail msg => error msg of
    20.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Nov 29 14:43:10 2014 +0100
    20.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sun Nov 30 12:24:56 2014 +0100
    20.3 @@ -462,8 +462,8 @@
    20.4        | decode ps (Ast.Appl asts) = decode_appl ps asts;
    20.5  
    20.6      val source = Syntax.read_token str;
    20.7 -    val (pos, _) = #range source;
    20.8 -    val syms = Symbol_Pos.source_explode source;
    20.9 +    val pos = Input.pos_of source;
   20.10 +    val syms = Input.source_explode source;
   20.11      val ast =
   20.12        parse_asts ctxt true root (syms, pos)
   20.13        |> uncurry (report_result ctxt pos)
    21.1 --- a/src/Pure/Thy/latex.ML	Sat Nov 29 14:43:10 2014 +0100
    21.2 +++ b/src/Pure/Thy/latex.ML	Sun Nov 30 12:24:56 2014 +0100
    21.3 @@ -132,8 +132,8 @@
    21.4        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
    21.5      else if Token.is_kind Token.Verbatim tok then
    21.6        let
    21.7 -        val {text, range = (pos, _), ...} = Token.source_position_of tok;
    21.8 -        val ants = Antiquote.read (Symbol_Pos.explode (text, pos), pos);
    21.9 +        val source = Token.source_position_of tok;
   21.10 +        val ants = Antiquote.read (Input.source_explode source, Input.pos_of source);
   21.11          val out = implode (map output_syms_antiq ants);
   21.12        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
   21.13      else if Token.is_kind Token.Cartouche tok then
    22.1 --- a/src/Pure/Thy/thy_output.ML	Sat Nov 29 14:43:10 2014 +0100
    22.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Nov 30 12:24:56 2014 +0100
    22.3 @@ -23,7 +23,7 @@
    22.4    val boolean: string -> bool
    22.5    val integer: string -> int
    22.6    val eval_antiq: Toplevel.state -> Antiquote.antiq -> string
    22.7 -  val check_text: Symbol_Pos.source -> Toplevel.state -> unit
    22.8 +  val check_text: Input.source -> Toplevel.state -> unit
    22.9    val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
   22.10    val pretty_text: Proof.context -> string -> Pretty.T
   22.11    val pretty_term: Proof.context -> term -> Pretty.T
   22.12 @@ -33,8 +33,8 @@
   22.13      Token.src -> 'a list -> Pretty.T list
   22.14    val output: Proof.context -> Pretty.T list -> string
   22.15    val verbatim_text: Proof.context -> string -> string
   22.16 -  val old_header_command: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
   22.17 -  val document_command: (xstring * Position.T) option * Symbol_Pos.source ->
   22.18 +  val old_header_command: Input.source -> Toplevel.transition -> Toplevel.transition
   22.19 +  val document_command: (xstring * Position.T) option * Input.source ->
   22.20      Toplevel.transition -> Toplevel.transition
   22.21  end;
   22.22  
   22.23 @@ -192,10 +192,10 @@
   22.24      val _ = Position.reports (maps words ants);
   22.25    in implode (map expand ants) end;
   22.26  
   22.27 -fun check_text ({delimited, text, range}: Symbol_Pos.source) state =
   22.28 - (Position.report (fst range) (Markup.language_document delimited);
   22.29 +fun check_text source state =
   22.30 + (Position.report (Input.pos_of source) (Markup.language_document (Input.is_delimited source));
   22.31    if Toplevel.is_skipped_proof state then ()
   22.32 -  else ignore (eval_antiquote state (text, fst range)));
   22.33 +  else ignore (eval_antiquote state (Input.text_of source, Input.pos_of source)));
   22.34  
   22.35  
   22.36  
   22.37 @@ -377,8 +377,11 @@
   22.38            Token.is_command tok andalso pred keywords (Token.content_of tok))) --
   22.39        Scan.repeat tag --
   22.40        Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
   22.41 -      >> (fn (((tok, pos'), tags), {text, range = (pos, _), ...}) =>
   22.42 -        let val name = Token.content_of tok
   22.43 +      >> (fn (((tok, pos'), tags), source) =>
   22.44 +        let
   22.45 +          val name = Token.content_of tok;
   22.46 +          val text = Input.text_of source;
   22.47 +          val pos = Input.pos_of source;
   22.48          in (SOME (name, pos', tags), (mk (name, (text, pos)), (flag, d))) end));
   22.49  
   22.50      val command = Scan.peek (fn d =>
   22.51 @@ -389,8 +392,8 @@
   22.52          in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
   22.53  
   22.54      val cmt = Scan.peek (fn d =>
   22.55 -      Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source)
   22.56 -      >> (fn {text, range = (pos, _), ...} => (NONE, (MarkupToken ("cmt", (text, pos)), ("", d)))));
   22.57 +      Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) >> (fn source =>
   22.58 +        (NONE, (MarkupToken ("cmt", (Input.text_of source, Input.pos_of source)), ("", d)))));
   22.59  
   22.60      val other = Scan.peek (fn d =>
   22.61         Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
   22.62 @@ -487,9 +490,8 @@
   22.63  
   22.64  fun pretty_text_report ctxt source =
   22.65    let
   22.66 -    val {delimited, range = (pos, _), ...} = source;
   22.67 -    val _ = Context_Position.report ctxt pos (Markup.language_text delimited);
   22.68 -    val (s, _) = Symbol_Pos.source_content source;
   22.69 +    val (s, pos) = Input.source_content source;
   22.70 +    val _ = Context_Position.report ctxt pos (Markup.language_text (Input.is_delimited source));
   22.71    in pretty_text ctxt s end;
   22.72  
   22.73  fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
   22.74 @@ -669,8 +671,8 @@
   22.75  
   22.76  fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position)
   22.77    (fn {context = ctxt, ...} => fn source =>
   22.78 -   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#1 (#range source)) (ml source);
   22.79 -    Symbol_Pos.source_content source |> #1
   22.80 +   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
   22.81 +    Input.source_content source |> #1
   22.82      |> verbatim_text ctxt));
   22.83  
   22.84  fun ml_enclose bg en source =
   22.85 @@ -690,7 +692,7 @@
   22.86    ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
   22.87      (fn source =>
   22.88        ML_Lex.read Position.none ("ML_Env.check_functor " ^
   22.89 -        ML_Syntax.print_string (#1 (Symbol_Pos.source_content source)))) #>
   22.90 +        ML_Syntax.print_string (#1 (Input.source_content source)))) #>
   22.91  
   22.92    ml_text @{binding ML_text} (K []));
   22.93  
    23.1 --- a/src/Pure/Thy/thy_syntax.ML	Sat Nov 29 14:43:10 2014 +0100
    23.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sun Nov 30 12:24:56 2014 +0100
    23.3 @@ -26,9 +26,8 @@
    23.4  
    23.5  fun reports_of_token tok =
    23.6    let
    23.7 -    val {text, range = (pos, _), ...} = Token.source_position_of tok;
    23.8      val malformed_symbols =
    23.9 -      Symbol_Pos.explode (text, pos)
   23.10 +      Input.source_explode (Token.source_position_of tok)
   23.11        |> map_filter (fn (sym, pos) =>
   23.12            if Symbol.is_malformed sym
   23.13            then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
    24.1 --- a/src/Pure/Tools/rail.ML	Sat Nov 29 14:43:10 2014 +0100
    24.2 +++ b/src/Pure/Tools/rail.ML	Sun Nov 30 12:24:56 2014 +0100
    24.3 @@ -281,11 +281,10 @@
    24.4  
    24.5  (* read *)
    24.6  
    24.7 -fun read ctxt (source: Symbol_Pos.source) =
    24.8 +fun read ctxt source =
    24.9    let
   24.10 -    val {text, range = (pos, _), ...} = source;
   24.11 -    val _ = Context_Position.report ctxt pos Markup.language_rail;
   24.12 -    val toks = tokenize (Symbol_Pos.explode (text, pos));
   24.13 +    val _ = Context_Position.report ctxt (Input.pos_of source) Markup.language_rail;
   24.14 +    val toks = tokenize (Input.source_explode source);
   24.15      val _ = Context_Position.reports ctxt (maps reports_of_token toks);
   24.16      val rules = parse_rules toks;
   24.17      val _ = Position.reports (maps (reports_of_tree ctxt o #2) rules);