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