tuned signature -- prefer quasi-abstract Symbol_Pos.source;

--- a/src/Pure/General/symbol_pos.ML	Wed Aug 27 12:32:07 2014 +0200
+++ b/src/Pure/General/symbol_pos.ML	Wed Aug 27 12:32:42 2014 +0200
@@ -41,6 +41,7 @@
   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_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
@@ -261,6 +262,8 @@
 
 type source = {delimited: bool, text: text, pos: Position.T};
 
+fun source_explode {delimited = _, text, pos} = explode (text, pos);
+
 fun source_content {delimited = _, text, pos} =
   let val syms = explode (text, pos) in (content syms, pos) end;
 

--- a/src/Pure/Isar/attrib.ML	Wed Aug 27 12:32:07 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Aug 27 12:32:42 2014 +0200
@@ -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.text * Position.T -> Token.src list
+  val read_attribs: Proof.context -> Symbol_Pos.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
@@ -286,14 +286,14 @@
     val _ = map (attribute ctxt) srcs;
   in srcs end;
 
-fun read_attribs ctxt (text, pos) =
+fun read_attribs ctxt source =
   let
+    val syms = Symbol_Pos.source_explode source;
     val lex = #1 (Keyword.get_lexicons ());
-    val syms = Symbol_Pos.explode (text, pos);
   in
-    (case Token.read lex Parse.attribs (syms, pos) of
+    (case Token.read lex Parse.attribs (syms, #pos source) of
       [raw_srcs] => check_attribs ctxt raw_srcs
-    | _ => error ("Malformed attributes" ^ Position.here pos))
+    | _ => error ("Malformed attributes" ^ Position.here (#pos source)))
   end;
 
 

--- a/src/Pure/Syntax/syntax.ML	Wed Aug 27 12:32:07 2014 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Aug 27 12:32:42 2014 +0200
@@ -185,10 +185,10 @@
   let
     fun parse_tree tree =
       let
-        val {delimited, text, pos} = token_source tree;
-        val syms = Symbol_Pos.explode (text, pos);
-        val _ = Context_Position.report ctxt pos (markup delimited);
-      in parse (syms, pos) end;
+        val source = token_source tree;
+        val syms = Symbol_Pos.source_explode source;
+        val _ = Context_Position.report ctxt (#pos source) (markup (#delimited source));
+      in parse (syms, #pos source) end;
   in
     (case YXML.parse_body str handle Fail msg => error msg of
       body as [tree as XML.Elem ((name, _), _)] =>

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Aug 27 12:32:07 2014 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Aug 27 12:32:42 2014 +0200
@@ -461,11 +461,11 @@
           else decode_appl ps asts
       | decode ps (Ast.Appl asts) = decode_appl ps asts;
 
-    val {text, pos, ...} = Syntax.read_token str;
-    val syms = Symbol_Pos.explode (text, pos);
+    val source = Syntax.read_token str;
+    val syms = Symbol_Pos.source_explode source;
     val ast =
-      parse_asts ctxt true root (syms, pos)
-      |> uncurry (report_result ctxt pos)
+      parse_asts ctxt true root (syms, #pos source)
+      |> uncurry (report_result ctxt (#pos source))
       |> decode [];
     val _ = Context_Position.reports_text ctxt (! reports);
   in ast end;