src/Pure/Isar/outer_lex.ML

   val is_begin_ignore: token -> bool
   val is_end_ignore: token -> bool
   val is_blank: token -> bool
   val is_newline: token -> bool
   val source_of: token -> string
+  val source_of': token -> SymbolPos.text * Position.T
   val content_of: token -> string
   val unparse: token -> string
   val text_of: token -> string * string
   val get_value: token -> value option
   val map_value: (value -> value) -> token -> token

 (* token content *)
 
 fun source_of (Token ((source, (pos, _)), _, _)) =
   YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
 
+fun source_of' (Token ((source, (pos, _)), _, _)) = (source, pos);
+
 fun content_of (Token (_, (_, x), _)) = x;
 
 
 (* unparse *)