diff -r a7d175c48228 -r bd8813d7774d src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sun Mar 22 19:10:58 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sun Mar 22 19:10:59 2009 +0100
@@ -13,9 +13,10 @@
   val stopper: token Scan.stopper
   val is_regular: token -> bool
   val is_improper: token -> bool
-  val pos_of: token -> string
+  val pos_of: token -> Position.T
   val kind_of: token -> token_kind
   val content_of: token -> string
+  val text_of: token -> string
   val markup_of: token -> Markup.T
   val report_token: token -> unit
   val keywords: string list
@@ -42,10 +43,8 @@
 
 (* position *)
 
-fun position_of (Token ((pos, _), _)) = pos;
-fun end_position_of (Token ((_, pos), _)) = pos;
-
-val pos_of = Position.str_of o position_of;
+fun pos_of (Token ((pos, _), _)) = pos;
+fun end_pos_of (Token ((_, pos), _)) = pos;
 
 
 (* control tokens *)
@@ -57,7 +56,7 @@
   | is_eof _ = false;
 
 val stopper =
-  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
+  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
 
 
 (* token content *)
@@ -67,6 +66,11 @@
 
 fun kind_of (Token (_, (k, _))) = k;
 
+fun text_of tok =
+  (case kind_of tok of
+    Error msg => error (msg ^ Position.str_of (pos_of tok))
+  | _ => Symbol.escape (content_of tok));
+
 fun is_regular (Token (_, (Error _, _))) = false
   | is_regular (Token (_, (EOF, _))) = false
   | is_regular _ = true;
@@ -93,7 +97,7 @@
     | Error _   => Markup.ML_malformed
     | EOF       => Markup.none);
 
-fun report_token tok = Position.report (markup_of tok) (position_of tok);
+fun report_token tok = Position.report (markup_of tok) (pos_of tok);