added source_of';

--- a/src/Pure/Isar/outer_lex.ML	Thu Aug 14 19:52:37 2008 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Thu Aug 14 19:52:39 2008 +0200
@@ -36,6 +36,7 @@
   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
@@ -183,6 +184,8 @@
 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;