# HG changeset patch
# User wenzelm
# Date 1393712257 -3600
# Node ID b7bdea5336dd68ca83b7a3235fe6bb533627f0da
# Parent  42ac3cfb89f6582d80ddb849eaa3e08903f76b1a
tuned signature;

diff -r 42ac3cfb89f6 -r b7bdea5336dd src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sat Mar 01 22:46:31 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sat Mar 01 23:17:37 2014 +0100
@@ -37,10 +37,11 @@
   val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
     (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
   type text = string
-  type source = {delimited: bool, text: text, pos: Position.T}
   val implode: T list -> text
   val implode_range: Position.T -> Position.T -> T list -> text * Position.range
   val explode: text * Position.T -> T list
+  type source = {delimited: bool, text: text, pos: Position.T}
+  val source_content: source -> string * Position.T
   val scan_ident: T list -> T list * T list
   val is_identifier: string -> bool
 end;
@@ -233,7 +234,6 @@
 (* compact representation -- with Symbol.DEL padding *)
 
 type text = string;
-type source = {delimited: bool, text: text, pos: Position.T}
 
 fun pad [] = []
   | pad [(s, _)] = [s]
@@ -257,6 +257,14 @@
   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, pos: Position.T};
+
+fun source_content {delimited = _, text, pos} =
+  let val syms = explode (text, pos) in (content syms, pos) end;
+
+
 (* identifiers *)
 
 local
diff -r 42ac3cfb89f6 -r b7bdea5336dd src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 01 22:46:31 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 01 23:17:37 2014 +0100
@@ -377,9 +377,8 @@
 fun read_class ctxt text =
   let
     val tsig = tsig_of ctxt;
-    val {text, pos, ...} = Syntax.read_token_source text;
-    val syms = Symbol_Pos.explode (text, pos);
-    val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
+    val (s, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+    val c = Type.cert_class tsig (Type.intern_class tsig s)
       handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
     val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
   in c end;
@@ -460,7 +459,7 @@
 fun read_type_name ctxt strict text =
   let
     val tsig = tsig_of ctxt;
-    val (c, pos) = Syntax.read_token_content text;
+    val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
   in
     if Lexicon.is_tid c then
      (Context_Position.report ctxt pos Markup.tfree;
@@ -486,11 +485,11 @@
 
 
 fun read_const_proper ctxt strict =
-  prep_const_proper ctxt strict o Syntax.read_token_content;
+  prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;
 
 fun read_const ctxt strict ty text =
   let
-    val (c, pos) = Syntax.read_token_content text;
+    val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
     val _ = no_skolem false c;
   in
     (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
diff -r 42ac3cfb89f6 -r b7bdea5336dd src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Mar 01 22:46:31 2014 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Mar 01 23:17:37 2014 +0100
@@ -15,8 +15,7 @@
   val ambiguity_limit_raw: Config.raw
   val ambiguity_limit: int Config.T
   val read_token_pos: string -> Position.T
-  val read_token_source: string -> Symbol_Pos.source
-  val read_token_content: string -> string * Position.T
+  val read_token: string -> Symbol_Pos.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
@@ -178,13 +177,7 @@
 
 fun read_token_pos str = #2 (token_position (YXML.parse str handle Fail msg => error msg));
 
-fun read_token_source str = token_source (YXML.parse str handle Fail msg => error msg);
-
-fun read_token_content str =
-  let
-    val {text, pos, ...} = read_token_source str;
-    val syms = Symbol_Pos.explode (text, pos);
-  in (Symbol_Pos.content syms, pos) end;
+fun read_token str = token_source (YXML.parse str handle Fail msg => error msg);
 
 fun parse_token ctxt decode markup parse str =
   let
diff -r 42ac3cfb89f6 -r b7bdea5336dd src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Mar 01 22:46:31 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Mar 01 23:17:37 2014 +0100
@@ -440,7 +440,7 @@
           else decode_appl ps asts
       | decode ps (Ast.Appl asts) = decode_appl ps asts;
 
-    val {text, pos, ...} = Syntax.read_token_source str;
+    val {text, pos, ...} = Syntax.read_token str;
     val syms = Symbol_Pos.explode (text, pos);
     val ast =
       parse_asts ctxt true root (syms, pos)
diff -r 42ac3cfb89f6 -r b7bdea5336dd src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Mar 01 22:46:31 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Mar 01 23:17:37 2014 +0100
@@ -467,10 +467,11 @@
 fun pretty_text ctxt =
   Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
 
-fun pretty_text_report ctxt {delimited, text, pos} =
+fun pretty_text_report ctxt source =
   let
+    val {delimited, pos, ...} = source;
     val _ = Context_Position.report ctxt pos (Markup.language_text delimited);
-    val s = Symbol_Pos.content (Symbol_Pos.explode (text, pos));
+    val (s, _) = Symbol_Pos.source_content source;
   in pretty_text ctxt s end;
 
 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
@@ -641,9 +642,10 @@
 local
 
 fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
-  (fn {context, ...} => fn source as {text, pos, ...} =>
-   (ML_Context.eval_in (SOME context) false pos (ml source);
-    Symbol_Pos.content (Symbol_Pos.explode (text, pos))
+  (fn {context, ...} => fn source =>
+   (ML_Context.eval_in (SOME context) false (#pos source) (ml source);
+    Symbol_Pos.source_content source
+    |> #1
     |> (if Config.get context quotes then quote else I)
     |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
         else verb_text)));
@@ -663,9 +665,9 @@
     (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
 
   ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
-    (fn {text, pos, ...} =>
+    (fn source =>
       ML_Lex.read Position.none ("ML_Env.check_functor " ^
-        ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (text, pos))))) #>
+        ML_Syntax.print_string (#1 (Symbol_Pos.source_content source)))) #>
 
   ml_text (Binding.name "ML_text") (K []));