# HG changeset patch
# User wenzelm
# Date 1417346696 -3600
# Node ID a8bcb5a446c8b645b9e45c6e1c0e25dcd07e5ea3
# Parent  b3c45d0e4fe1b4652f50c9640078024184d3e97f
more abstract type Input.source;

diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -69,7 +69,7 @@
   | _ => error ("Single ML name expected in input: " ^ quote txt));
 
 fun prep_ml source =
-  (#1 (Symbol_Pos.source_content source), ML_Lex.read_source false source);
+  (#1 (Input.source_content source), ML_Lex.read_source false source);
 
 fun index_ml name kind ml = Thy_Output.antiquotation name
   (Scan.lift (Args.text_source_position -- Scan.option (Args.colon |-- Args.text_source_position)))
@@ -90,7 +90,7 @@
         else txt1 ^ " : " ^ txt2;
       val txt' = if kind = "" then txt else kind ^ " " ^ txt;
 
-      val (pos, _) = #range source1;
+      val pos = Input.pos_of 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 b3c45d0e4fe1 -r a8bcb5a446c8 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sun Nov 30 12:24:56 2014 +0100
@@ -146,8 +146,7 @@
           ML_Lex.read Position.none "fn _ => (" @
           ML_Lex.read_source false source @
           ML_Lex.read Position.none ");";
-        val (pos, _) = #range source;
-        val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags pos toks;
+        val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks;
       in "" end);
 *}
 
@@ -204,7 +203,7 @@
 structure ML_Tactic:
 sig
   val set: (Proof.context -> tactic) -> Proof.context -> Proof.context
-  val ml_tactic: Symbol_Pos.source -> Proof.context -> tactic
+  val ml_tactic: Input.source -> Proof.context -> tactic
 end =
 struct
   structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac);
@@ -214,7 +213,7 @@
   fun ml_tactic source ctxt =
     let
       val ctxt' = ctxt |> Context.proof_map
-        (ML_Context.expression (#range source) "tactic" "Proof.context -> tactic"
+        (ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic"
           "Context.map_proof (ML_Tactic.set tactic)"
           (ML_Lex.read Position.none "fn ctxt: Proof.context =>" @
            ML_Lex.read_source false source));
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/General/input.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/input.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -0,0 +1,43 @@
+(*  Title:      Pure/General/input.ML
+    Author:     Makarius
+
+Generic input with position information.
+*)
+
+signature INPUT =
+sig
+  type source
+  val is_delimited: source -> bool
+  val text_of: source -> Symbol_Pos.text
+  val pos_of: source -> Position.T
+  val range_of: source -> Position.range
+  val source: bool -> Symbol_Pos.text -> Position.range -> source
+  val source_explode: source -> Symbol_Pos.T list
+  val source_content: source -> string * Position.T
+end;
+
+structure Input: INPUT =
+struct
+
+abstype source = Source of {delimited: bool, text: Symbol_Pos.text, range: Position.range}
+with
+
+fun is_delimited (Source {delimited, ...}) = delimited;
+fun text_of (Source {text, ...}) = text;
+fun pos_of (Source {range = (pos, _), ...}) = pos;
+fun range_of (Source {range, ...}) = range;
+
+fun source delimited text range =
+  Source {delimited = delimited, text = text, range = range};
+
+fun source_explode (Source {text, range = (pos, _), ...}) =
+  Symbol_Pos.explode (text, pos);
+
+fun source_content (Source {text, range = (pos, _), ...}) =
+  let val syms = Symbol_Pos.explode (text, pos)
+  in (Symbol_Pos.content syms, pos) end;
+
+end;
+
+end;
+
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -39,9 +39,6 @@
   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, 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
   val is_identifier: string -> bool
 end;
@@ -253,16 +250,6 @@
   in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
 
 
-(* full source information *)
-
-type source = {delimited: bool, text: text, range: Position.range};
-
-fun source_explode {delimited = _, text, range = (pos, _)} = explode (text, pos);
-
-fun source_content {delimited = _, text, range = (pos, _)} =
-  let val syms = explode (text, pos) in (content syms, pos) end;
-
-
 (* identifiers *)
 
 local
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/args.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -22,11 +22,11 @@
   val mode: string -> bool parser
   val maybe: 'a parser -> 'a option parser
   val cartouche_inner_syntax: string parser
-  val cartouche_source_position: Symbol_Pos.source parser
-  val text_source_position: Symbol_Pos.source parser
+  val cartouche_source_position: Input.source parser
+  val text_source_position: Input.source parser
   val text: string parser
   val name_inner_syntax: string parser
-  val name_source_position: Symbol_Pos.source parser
+  val name_source_position: Input.source parser
   val name: string parser
   val binding: binding parser
   val alt_name: string parser
@@ -46,7 +46,7 @@
   val named_fact: (string -> string option * thm list) -> thm list parser
   val named_attribute: (string * Position.T -> morphism -> attribute) ->
     (morphism -> attribute) parser
-  val text_declaration: (Symbol_Pos.source -> declaration) -> declaration parser
+  val text_declaration: (Input.source -> declaration) -> declaration parser
   val typ_abbrev: typ context_parser
   val typ: typ context_parser
   val term: term context_parser
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -41,7 +41,7 @@
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val local_setup: Binding.binding -> attribute context_parser -> string ->
     local_theory -> local_theory
-  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
+  val attribute_setup: bstring * Position.T -> Input.source -> string ->
     local_theory -> local_theory
   val internal: (morphism -> attribute) -> Token.src
   val add_del: attribute -> attribute -> attribute context_parser
@@ -49,7 +49,7 @@
   val thms: thm list context_parser
   val multi_thm: thm list context_parser
   val check_attribs: Proof.context -> Token.src list -> Token.src list
-  val read_attribs: Proof.context -> Symbol_Pos.source -> Token.src list
+  val read_attribs: Proof.context -> Input.source -> Token.src list
   val transform_facts: morphism ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     (Attrib.binding * (thm list * Token.src list) list) list
@@ -208,7 +208,7 @@
 
 fun attribute_setup name source comment =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source) "parser" "Thm.attribute context_parser"
+  |> ML_Context.expression (Input.range_of source) "parser" "Thm.attribute context_parser"
     ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
       " parser " ^ ML_Syntax.print_string comment ^ ")")
   |> Context.proof_map;
@@ -287,11 +287,11 @@
 fun read_attribs ctxt source =
   let
     val keywords = Thy_Header.get_keywords' ctxt;
-    val syms = Symbol_Pos.source_explode source;
+    val syms = Input.source_explode source;
   in
     (case Token.read_no_commands keywords Parse.attribs syms of
       [raw_srcs] => check_attribs ctxt raw_srcs
-    | _ => error ("Malformed attributes" ^ Position.here (#1 (#range source))))
+    | _ => error ("Malformed attributes" ^ Position.here (Input.pos_of source)))
   end;
 
 
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -6,20 +6,19 @@
 
 signature ISAR_CMD =
 sig
-  val global_setup: Symbol_Pos.source -> theory -> theory
-  val local_setup: Symbol_Pos.source -> Proof.context -> Proof.context
-  val parse_ast_translation: Symbol_Pos.source -> theory -> theory
-  val parse_translation: Symbol_Pos.source -> theory -> theory
-  val print_translation: Symbol_Pos.source -> theory -> theory
-  val typed_print_translation: Symbol_Pos.source -> theory -> theory
-  val print_ast_translation: Symbol_Pos.source -> theory -> theory
+  val global_setup: Input.source -> theory -> theory
+  val local_setup: Input.source -> Proof.context -> Proof.context
+  val parse_ast_translation: Input.source -> theory -> theory
+  val parse_translation: Input.source -> theory -> theory
+  val print_translation: Input.source -> theory -> theory
+  val typed_print_translation: Input.source -> theory -> theory
+  val print_ast_translation: Input.source -> theory -> theory
   val translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
-  val oracle: bstring * Position.range -> Symbol_Pos.source -> theory -> theory
+  val oracle: bstring * Position.range -> Input.source -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
-  val declaration: {syntax: bool, pervasive: bool} ->
-    Symbol_Pos.source -> local_theory -> local_theory
-  val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
+  val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
+  val simproc_setup: string * Position.T -> string list -> Input.source ->
     string list -> local_theory -> local_theory
   val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
@@ -32,7 +31,7 @@
   val immediate_proof: Toplevel.transition -> Toplevel.transition
   val done_proof: Toplevel.transition -> Toplevel.transition
   val skip_proof: Toplevel.transition -> Toplevel.transition
-  val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
+  val ml_diag: bool -> Input.source -> Toplevel.transition -> Toplevel.transition
   val diag_state: Proof.context -> Toplevel.state
   val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
   val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
@@ -60,13 +59,13 @@
 
 fun global_setup source =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source) "setup" "theory -> theory"
+  |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
     "Context.map_theory setup"
   |> Context.theory_map;
 
 fun local_setup source =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source) "local_setup" "local_theory -> local_theory"
+  |> ML_Context.expression (Input.range_of source) "local_setup" "local_theory -> local_theory"
     "Context.map_proof local_setup"
   |> Context.proof_map;
 
@@ -75,35 +74,35 @@
 
 fun parse_ast_translation source =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source) "parse_ast_translation"
+  |> ML_Context.expression (Input.range_of source) "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 (#range source) "parse_translation"
+  |> ML_Context.expression (Input.range_of source) "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 (#range source) "print_translation"
+  |> ML_Context.expression (Input.range_of source) "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 (#range source) "typed_print_translation"
+  |> ML_Context.expression (Input.range_of source) "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 (#range source) "print_ast_translation"
+  |> ML_Context.expression (Input.range_of source) "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;
@@ -129,7 +128,7 @@
 
 fun oracle (name, range) source =
   let
-    val body_range = #range source;
+    val body_range = Input.range_of source;
     val body = ML_Lex.read_source false source;
 
     val hidden = ML_Lex.read Position.none;
@@ -164,7 +163,7 @@
 
 fun declaration {syntax, pervasive} source =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source) "declaration" "Morphism.declaration"
+  |> ML_Context.expression (Input.range_of source) "declaration" "Morphism.declaration"
     ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
       \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
   |> Context.proof_map;
@@ -174,7 +173,7 @@
 
 fun simproc_setup name lhss source identifier =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source) "proc"
+  |> ML_Context.expression (Input.range_of source) "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 b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -208,7 +208,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, range = (pos, pos)};
+          val source = Input.source true (cat_lines lines) (pos, pos);
           val flags = {SML = true, exchange = false, redirect = true, verbose = true};
         in
           thy' |> Context.theory_map
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/method.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -61,8 +61,7 @@
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
   val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
     local_theory -> local_theory
-  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
-    local_theory -> local_theory
+  val method_setup: bstring * Position.T -> Input.source -> string -> local_theory -> local_theory
   val method: Proof.context -> Token.src -> Proof.context -> method
   val method_closure: Proof.context -> Token.src -> Token.src
   val method_cmd: Proof.context -> Token.src -> Proof.context -> method
@@ -282,7 +281,7 @@
     Scan.lift (Args.text_declaration (fn source =>
       let
         val context' = context |>
-          ML_Context.expression (#range source)
+          ML_Context.expression (Input.range_of source)
             "tactic" "Morphism.morphism -> thm list -> tactic"
             "Method.set_tactic tactic"
             (ML_Lex.read Position.none "fn morphism: Morphism.morphism => fn facts: thm list =>" @
@@ -381,7 +380,7 @@
 
 fun method_setup name source comment =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source) "parser"
+  |> ML_Context.expression (Input.range_of source) "parser"
     "(Proof.context -> Proof.method) context_parser"
     ("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
       " parser " ^ ML_Syntax.print_string comment ^ ")")
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/parse.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -16,7 +16,7 @@
   val token: 'a parser -> Token.T parser
   val range: 'a parser -> ('a * Position.range) parser
   val position: 'a parser -> ('a * Position.T) parser
-  val source_position: 'a parser -> Symbol_Pos.source parser
+  val source_position: 'a parser -> Input.source parser
   val inner_syntax: 'a parser -> string parser
   val command_: string parser
   val keyword: string parser
@@ -92,8 +92,8 @@
   val simple_fixes: (binding * string option) list parser
   val fixes: (binding * string option * mixfix) list parser
   val for_fixes: (binding * string option * mixfix) list parser
-  val ML_source: Symbol_Pos.source parser
-  val document_source: Symbol_Pos.source parser
+  val ML_source: Input.source parser
+  val document_source: Input.source parser
   val term_group: string parser
   val prop_group: string parser
   val term: string parser
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -403,7 +403,7 @@
 
 fun read_class ctxt text =
   let
-    val (c, reports) = check_class ctxt (Symbol_Pos.source_content (Syntax.read_token text));
+    val (c, reports) = check_class ctxt (Input.source_content (Syntax.read_token text));
     val _ = Position.reports reports;
   in c end;
 
@@ -471,7 +471,7 @@
 fun read_type_name ctxt flags text =
   let
     val (T, reports) =
-      check_type_name ctxt flags (Symbol_Pos.source_content (Syntax.read_token text));
+      check_type_name ctxt flags (Input.source_content (Syntax.read_token text));
     val _ = Position.reports reports;
   in T end;
 
@@ -519,7 +519,7 @@
 
 fun read_const ctxt flags text =
   let
-    val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+    val (xname, pos) = Input.source_content (Syntax.read_token text);
     val (t, reports) = check_const ctxt flags (xname, [pos]);
     val _ = Position.reports reports;
   in t end;
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/token.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -52,7 +52,7 @@
   val is_blank: T -> bool
   val is_newline: T -> bool
   val inner_syntax_of: T -> string
-  val source_position_of: T -> Symbol_Pos.source
+  val source_position_of: T -> Input.source
   val content_of: T -> string
   val keyword_markup: bool * Markup.T -> string -> Markup.T
   val completion_report: T -> Position.report_text list
@@ -269,7 +269,7 @@
     in YXML.string_of tree end;
 
 fun source_position_of (Token ((source, range), (kind, _), _)) =
-  {delimited = delimited_kind kind, text = source, range = range};
+  Input.source (delimited_kind kind) source range;
 
 fun content_of (Token (_, (_, x), _)) = x;
 
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -34,10 +34,10 @@
 
 val _ = Theory.setup
  (ML_Antiquotation.value @{binding source}
-    (Scan.lift Args.text_source_position >> (fn {delimited, text, range} =>
-      "{delimited = " ^ Bool.toString delimited ^
-      ", text = " ^ ML_Syntax.print_string text ^
-      ", range = " ^ ML_Syntax.print_range range ^ "}")));
+    (Scan.lift Args.text_source_position >> (fn source =>
+      "Input.source " ^ Bool.toString (Input.is_delimited source) ^ " " ^
+        ML_Syntax.print_string (Input.text_of source) ^ " " ^
+        ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
 
 
 (* formal entities *)
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -21,10 +21,10 @@
     Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
   val eval_file: ML_Compiler.flags -> Path.T -> unit
-  val eval_source: ML_Compiler.flags -> Symbol_Pos.source -> unit
+  val eval_source: ML_Compiler.flags -> Input.source -> unit
   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 eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit
   val expression: Position.range -> string -> string -> string ->
     ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
 end
@@ -173,7 +173,7 @@
   in eval flags pos (ML_Lex.read pos (File.read path)) end;
 
 fun eval_source flags source =
-  eval flags (#1 (#range source)) (ML_Lex.read_source (#SML flags) source);
+  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
 
 fun eval_in ctxt flags pos ants =
   Context.setmp_thread_data (Option.map Context.Proof ctxt)
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/ML/ml_file.ML
--- a/src/Pure/ML/ml_file.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ML/ml_file.ML	Sun Nov 30 12:24:56 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, range = (pos, pos)};
+          val source = Input.source true (cat_lines lines) (pos, pos);
           val flags = {SML = false, exchange = false, redirect = true, verbose = true};
         in
           gthy
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -27,7 +27,7 @@
   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
+  val read_source: bool -> Input.source -> token Antiquote.antiquote list
 end;
 
 structure ML_Lex: ML_LEX =
@@ -330,13 +330,15 @@
   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) =
+fun read_source SML source =
   let
+    val pos = Input.pos_of source;
     val language = if SML then Markup.language_SML else Markup.language_ML;
     val _ =
-      if Position.is_reported_range pos then Position.report pos (language delimited)
+      if Position.is_reported_range pos
+      then Position.report pos (language (Input.is_delimited source))
       else ();
-  in gen_read SML pos text end;
+  in gen_read SML pos (Input.text_of source) end;
 
 end;
 
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/ROOT
--- a/src/Pure/ROOT	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ROOT	Sun Nov 30 12:24:56 2014 +0100
@@ -81,6 +81,7 @@
     "General/graph.ML"
     "General/graph_display.ML"
     "General/heap.ML"
+    "General/input.ML"
     "General/integer.ML"
     "General/linear_set.ML"
     "General/long_name.ML"
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ROOT.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -32,6 +32,7 @@
 use "General/symbol.ML";
 use "General/position.ML";
 use "General/symbol_pos.ML";
+use "General/input.ML";
 use "General/antiquote.ML";
 use "ML/ml_lex.ML";
 use "ML/ml_parse.ML";
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -15,7 +15,7 @@
   val ambiguity_limit_raw: Config.raw
   val ambiguity_limit: int Config.T
   val read_token_pos: string -> Position.T
-  val read_token: string -> Symbol_Pos.source
+  val read_token: string -> Input.source
   val parse_token: Proof.context -> (XML.tree list -> 'a) ->
     (bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
   val parse_sort: Proof.context -> string -> sort
@@ -169,11 +169,11 @@
       else (false, Position.no_range)
   | token_range (XML.Text _) = (false, Position.no_range);
 
-fun token_source tree : Symbol_Pos.source =
+fun token_source tree : Input.source =
   let
     val text = XML.content_of [tree];
     val (delimited, range) = token_range tree;
-  in {delimited = delimited, text = text, range = range} end;
+  in Input.source delimited text range end;
 
 in
 
@@ -186,9 +186,9 @@
     fun parse_tree tree =
       let
         val source = token_source tree;
-        val syms = Symbol_Pos.source_explode source;
-        val (pos, _) = #range source;
-        val _ = Context_Position.report ctxt pos (markup (#delimited source));
+        val syms = Input.source_explode source;
+        val pos = Input.pos_of source;
+        val _ = Context_Position.report ctxt pos (markup (Input.is_delimited source));
       in parse (syms, pos) end;
   in
     (case YXML.parse_body str handle Fail msg => error msg of
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -462,8 +462,8 @@
       | 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 pos = Input.pos_of source;
+    val syms = Input.source_explode source;
     val ast =
       parse_asts ctxt true root (syms, pos)
       |> uncurry (report_result ctxt pos)
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Thy/latex.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -132,8 +132,8 @@
       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
     else if Token.is_kind Token.Verbatim tok then
       let
-        val {text, range = (pos, _), ...} = Token.source_position_of tok;
-        val ants = Antiquote.read (Symbol_Pos.explode (text, pos), pos);
+        val source = Token.source_position_of tok;
+        val ants = Antiquote.read (Input.source_explode source, Input.pos_of source);
         val out = implode (map output_syms_antiq ants);
       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
     else if Token.is_kind Token.Cartouche tok then
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -23,7 +23,7 @@
   val boolean: string -> bool
   val integer: string -> int
   val eval_antiq: Toplevel.state -> Antiquote.antiq -> string
-  val check_text: Symbol_Pos.source -> Toplevel.state -> unit
+  val check_text: Input.source -> Toplevel.state -> unit
   val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
   val pretty_text: Proof.context -> string -> Pretty.T
   val pretty_term: Proof.context -> term -> Pretty.T
@@ -33,8 +33,8 @@
     Token.src -> 'a list -> Pretty.T list
   val output: Proof.context -> Pretty.T list -> string
   val verbatim_text: Proof.context -> string -> string
-  val old_header_command: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
-  val document_command: (xstring * Position.T) option * Symbol_Pos.source ->
+  val old_header_command: Input.source -> Toplevel.transition -> Toplevel.transition
+  val document_command: (xstring * Position.T) option * Input.source ->
     Toplevel.transition -> Toplevel.transition
 end;
 
@@ -192,10 +192,10 @@
     val _ = Position.reports (maps words ants);
   in implode (map expand ants) end;
 
-fun check_text ({delimited, text, range}: Symbol_Pos.source) state =
- (Position.report (fst range) (Markup.language_document delimited);
+fun check_text source state =
+ (Position.report (Input.pos_of source) (Markup.language_document (Input.is_delimited source));
   if Toplevel.is_skipped_proof state then ()
-  else ignore (eval_antiquote state (text, fst range)));
+  else ignore (eval_antiquote state (Input.text_of source, Input.pos_of source)));
 
 
 
@@ -377,8 +377,11 @@
           Token.is_command tok andalso pred keywords (Token.content_of tok))) --
       Scan.repeat tag --
       Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
-      >> (fn (((tok, pos'), tags), {text, range = (pos, _), ...}) =>
-        let val name = Token.content_of tok
+      >> (fn (((tok, pos'), tags), source) =>
+        let
+          val name = Token.content_of tok;
+          val text = Input.text_of source;
+          val pos = Input.pos_of source;
         in (SOME (name, pos', tags), (mk (name, (text, pos)), (flag, d))) end));
 
     val command = Scan.peek (fn d =>
@@ -389,8 +392,8 @@
         in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
 
     val cmt = Scan.peek (fn d =>
-      Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source)
-      >> (fn {text, range = (pos, _), ...} => (NONE, (MarkupToken ("cmt", (text, pos)), ("", d)))));
+      Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) >> (fn source =>
+        (NONE, (MarkupToken ("cmt", (Input.text_of source, Input.pos_of source)), ("", d)))));
 
     val other = Scan.peek (fn d =>
        Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
@@ -487,9 +490,8 @@
 
 fun pretty_text_report ctxt source =
   let
-    val {delimited, range = (pos, _), ...} = source;
-    val _ = Context_Position.report ctxt pos (Markup.language_text delimited);
-    val (s, _) = Symbol_Pos.source_content source;
+    val (s, pos) = Input.source_content source;
+    val _ = Context_Position.report ctxt pos (Markup.language_text (Input.is_delimited source));
   in pretty_text ctxt s end;
 
 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
@@ -669,8 +671,8 @@
 
 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 (#1 (#range source)) (ml source);
-    Symbol_Pos.source_content source |> #1
+   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
+    Input.source_content source |> #1
     |> verbatim_text ctxt));
 
 fun ml_enclose bg en source =
@@ -690,7 +692,7 @@
   ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
     (fn source =>
       ML_Lex.read Position.none ("ML_Env.check_functor " ^
-        ML_Syntax.print_string (#1 (Symbol_Pos.source_content source)))) #>
+        ML_Syntax.print_string (#1 (Input.source_content source)))) #>
 
   ml_text @{binding ML_text} (K []));
 
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -26,9 +26,8 @@
 
 fun reports_of_token tok =
   let
-    val {text, range = (pos, _), ...} = Token.source_position_of tok;
     val malformed_symbols =
-      Symbol_Pos.explode (text, pos)
+      Input.source_explode (Token.source_position_of tok)
       |> map_filter (fn (sym, pos) =>
           if Symbol.is_malformed sym
           then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Tools/rail.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -281,11 +281,10 @@
 
 (* read *)
 
-fun read ctxt (source: Symbol_Pos.source) =
+fun read ctxt source =
   let
-    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.report ctxt (Input.pos_of source) Markup.language_rail;
+    val toks = tokenize (Input.source_explode source);
     val _ = Context_Position.reports ctxt (maps reports_of_token toks);
     val rules = parse_rules toks;
     val _ = Position.reports (maps (reports_of_tree ctxt o #2) rules);