# HG changeset patch
# User wenzelm
# Date 1218736359 -7200
# Node ID 34d61938e27a205ee1eebb8d4b064ac5a3074121
# Parent  631371a02b8c8d48f3604cf3a78bc0620d1a0abd
added source_of';

diff -r 631371a02b8c -r 34d61938e27a src/Pure/Isar/outer_lex.ML
--- 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;