# HG changeset patch
# User wenzelm
# Date 1243891685 -7200
# Node ID 9639a6d4d714a0750791282ded8bbb9f645fdbde
# Parent  e44f1e4fa1f472677b0d78826989f66838da5508
added flatten;

diff -r e44f1e4fa1f4 -r 9639a6d4d714 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Mon Jun 01 23:28:04 2009 +0200
+++ b/src/Pure/ML/ml_lex.ML	Mon Jun 01 23:28:05 2009 +0200
@@ -18,6 +18,7 @@
   val kind_of: token -> token_kind
   val content_of: token -> string
   val text_of: token -> string
+  val flatten: token list -> string
   val report_token: token -> unit
   val keywords: string list
   val source: (Symbol.symbol, 'a) Source.source ->
@@ -73,6 +74,8 @@
     Error msg => error msg
   | _ => Symbol.escape (content_of tok));
 
+val flatten = implode o map text_of;
+
 fun is_regular (Token (_, (Error _, _))) = false
   | is_regular (Token (_, (EOF, _))) = false
   | is_regular _ = true;