1.1 --- a/src/Pure/General/symbol_pos.ML	Sat Mar 01 22:46:31 2014 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Sat Mar 01 23:17:37 2014 +0100
     1.3 @@ -37,10 +37,11 @@
     1.4    val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
     1.5      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
     1.6    type text = string
     1.7 -  type source = {delimited: bool, text: text, pos: Position.T}
     1.8    val implode: T list -> text
     1.9    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
    1.10    val explode: text * Position.T -> T list
    1.11 +  type source = {delimited: bool, text: text, pos: Position.T}
    1.12 +  val source_content: source -> string * Position.T
    1.13    val scan_ident: T list -> T list * T list
    1.14    val is_identifier: string -> bool
    1.15  end;
    1.16 @@ -233,7 +234,6 @@
    1.17  (* compact representation -- with Symbol.DEL padding *)
    1.18  
    1.19  type text = string;
    1.20 -type source = {delimited: bool, text: text, pos: Position.T}
    1.21  
    1.22  fun pad [] = []
    1.23    | pad [(s, _)] = [s]
    1.24 @@ -257,6 +257,14 @@
    1.25    in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
    1.26  
    1.27  
    1.28 +(* full source information *)
    1.29 +
    1.30 +type source = {delimited: bool, text: text, pos: Position.T};
    1.31 +
    1.32 +fun source_content {delimited = _, text, pos} =
    1.33 +  let val syms = explode (text, pos) in (content syms, pos) end;
    1.34 +
    1.35 +
    1.36  (* identifiers *)
    1.37  
    1.38  local

     2.1 --- a/src/Pure/Isar/proof_context.ML	Sat Mar 01 22:46:31 2014 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Mar 01 23:17:37 2014 +0100
     2.3 @@ -377,9 +377,8 @@
     2.4  fun read_class ctxt text =
     2.5    let
     2.6      val tsig = tsig_of ctxt;
     2.7 -    val {text, pos, ...} = Syntax.read_token_source text;
     2.8 -    val syms = Symbol_Pos.explode (text, pos);
     2.9 -    val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
    2.10 +    val (s, pos) = Symbol_Pos.source_content (Syntax.read_token text);
    2.11 +    val c = Type.cert_class tsig (Type.intern_class tsig s)
    2.12        handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
    2.13      val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
    2.14    in c end;
    2.15 @@ -460,7 +459,7 @@
    2.16  fun read_type_name ctxt strict text =
    2.17    let
    2.18      val tsig = tsig_of ctxt;
    2.19 -    val (c, pos) = Syntax.read_token_content text;
    2.20 +    val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
    2.21    in
    2.22      if Lexicon.is_tid c then
    2.23       (Context_Position.report ctxt pos Markup.tfree;
    2.24 @@ -486,11 +485,11 @@
    2.25  
    2.26  
    2.27  fun read_const_proper ctxt strict =
    2.28 -  prep_const_proper ctxt strict o Syntax.read_token_content;
    2.29 +  prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;
    2.30  
    2.31  fun read_const ctxt strict ty text =
    2.32    let
    2.33 -    val (c, pos) = Syntax.read_token_content text;
    2.34 +    val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
    2.35      val _ = no_skolem false c;
    2.36    in
    2.37      (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of

     3.1 --- a/src/Pure/Syntax/syntax.ML	Sat Mar 01 22:46:31 2014 +0100
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Mar 01 23:17:37 2014 +0100
     3.3 @@ -15,8 +15,7 @@
     3.4    val ambiguity_limit_raw: Config.raw
     3.5    val ambiguity_limit: int Config.T
     3.6    val read_token_pos: string -> Position.T
     3.7 -  val read_token_source: string -> Symbol_Pos.source
     3.8 -  val read_token_content: string -> string * Position.T
     3.9 +  val read_token: string -> Symbol_Pos.source
    3.10    val parse_token: Proof.context -> (XML.tree list -> 'a) ->
    3.11      (bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
    3.12    val parse_sort: Proof.context -> string -> sort
    3.13 @@ -178,13 +177,7 @@
    3.14  
    3.15  fun read_token_pos str = #2 (token_position (YXML.parse str handle Fail msg => error msg));
    3.16  
    3.17 -fun read_token_source str = token_source (YXML.parse str handle Fail msg => error msg);
    3.18 -
    3.19 -fun read_token_content str =
    3.20 -  let
    3.21 -    val {text, pos, ...} = read_token_source str;
    3.22 -    val syms = Symbol_Pos.explode (text, pos);
    3.23 -  in (Symbol_Pos.content syms, pos) end;
    3.24 +fun read_token str = token_source (YXML.parse str handle Fail msg => error msg);
    3.25  
    3.26  fun parse_token ctxt decode markup parse str =
    3.27    let

     4.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Mar 01 22:46:31 2014 +0100
     4.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sat Mar 01 23:17:37 2014 +0100
     4.3 @@ -440,7 +440,7 @@
     4.4            else decode_appl ps asts
     4.5        | decode ps (Ast.Appl asts) = decode_appl ps asts;
     4.6  
     4.7 -    val {text, pos, ...} = Syntax.read_token_source str;
     4.8 +    val {text, pos, ...} = Syntax.read_token str;
     4.9      val syms = Symbol_Pos.explode (text, pos);
    4.10      val ast =
    4.11        parse_asts ctxt true root (syms, pos)

     5.1 --- a/src/Pure/Thy/thy_output.ML	Sat Mar 01 22:46:31 2014 +0100
     5.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Mar 01 23:17:37 2014 +0100
     5.3 @@ -467,10 +467,11 @@
     5.4  fun pretty_text ctxt =
     5.5    Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
     5.6  
     5.7 -fun pretty_text_report ctxt {delimited, text, pos} =
     5.8 +fun pretty_text_report ctxt source =
     5.9    let
    5.10 +    val {delimited, pos, ...} = source;
    5.11      val _ = Context_Position.report ctxt pos (Markup.language_text delimited);
    5.12 -    val s = Symbol_Pos.content (Symbol_Pos.explode (text, pos));
    5.13 +    val (s, _) = Symbol_Pos.source_content source;
    5.14    in pretty_text ctxt s end;
    5.15  
    5.16  fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
    5.17 @@ -641,9 +642,10 @@
    5.18  local
    5.19  
    5.20  fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
    5.21 -  (fn {context, ...} => fn source as {text, pos, ...} =>
    5.22 -   (ML_Context.eval_in (SOME context) false pos (ml source);
    5.23 -    Symbol_Pos.content (Symbol_Pos.explode (text, pos))
    5.24 +  (fn {context, ...} => fn source =>
    5.25 +   (ML_Context.eval_in (SOME context) false (#pos source) (ml source);
    5.26 +    Symbol_Pos.source_content source
    5.27 +    |> #1
    5.28      |> (if Config.get context quotes then quote else I)
    5.29      |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    5.30          else verb_text)));
    5.31 @@ -663,9 +665,9 @@
    5.32      (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
    5.33  
    5.34    ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
    5.35 -    (fn {text, pos, ...} =>
    5.36 +    (fn source =>
    5.37        ML_Lex.read Position.none ("ML_Env.check_functor " ^
    5.38 -        ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (text, pos))))) #>
    5.39 +        ML_Syntax.print_string (#1 (Symbol_Pos.source_content source)))) #>
    5.40  
    5.41    ml_text (Binding.name "ML_text") (K []));
    5.42