--- 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;