# HG changeset patch
# User wenzelm
# Date 1244129497 -7200
# Node ID 5c9dbd5115109ff1fd15b8c64c4758e251bb9307
# Parent  e8d5417a1831b5caffa08639f0015643628dac02
tuned signature;

diff -r e8d5417a1831 -r 5c9dbd511510 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Thu Jun 04 17:31:37 2009 +0200
+++ b/src/Pure/ML/ml_lex.ML	Thu Jun 04 17:31:37 2009 +0200
@@ -17,7 +17,7 @@
   val pos_of: token -> Position.T
   val kind_of: token -> token_kind
   val content_of: token -> string
-  val text_of: token -> string
+  val check_content_of: token -> string
   val flatten: token list -> string
   val report_token: token -> unit
   val keywords: string list
@@ -64,17 +64,17 @@
 
 (* token content *)
 
+fun kind_of (Token (_, (k, _))) = k;
+
 fun content_of (Token (_, (_, x))) = x;
 fun token_leq (tok, tok') = content_of tok <= content_of tok';
 
-fun kind_of (Token (_, (k, _))) = k;
-
-fun text_of tok =
+fun check_content_of tok =
   (case kind_of tok of
     Error msg => error msg
-  | _ => Symbol.escape (content_of tok));
+  | _ => content_of tok);
 
-val flatten = implode o map text_of;
+val flatten = implode o map (Symbol.escape o check_content_of);
 
 fun is_regular (Token (_, (Error _, _))) = false
   | is_regular (Token (_, (EOF, _))) = false
@@ -255,7 +255,7 @@
     |> Source.exhaust
     |> tap (List.app (Antiquote.report report_token))
     |> tap Antiquote.check_nesting
-    |> tap (List.app (fn Antiquote.Text tok => ignore (text_of tok) | _ => ())))
+    |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
   handle ERROR msg =>
     cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);