added flatten;
authorwenzelm
Mon Jun 01 23:28:05 2009 +0200 (2009-06-01)
changeset 313329639a6d4d714
parent 31331 e44f1e4fa1f4
child 31333 fcd010617e6c
added flatten;
src/Pure/ML/ml_lex.ML
     1.1 --- a/src/Pure/ML/ml_lex.ML	Mon Jun 01 23:28:04 2009 +0200
     1.2 +++ b/src/Pure/ML/ml_lex.ML	Mon Jun 01 23:28:05 2009 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    val kind_of: token -> token_kind
     1.5    val content_of: token -> string
     1.6    val text_of: token -> string
     1.7 +  val flatten: token list -> string
     1.8    val report_token: token -> unit
     1.9    val keywords: string list
    1.10    val source: (Symbol.symbol, 'a) Source.source ->
    1.11 @@ -73,6 +74,8 @@
    1.12      Error msg => error msg
    1.13    | _ => Symbol.escape (content_of tok));
    1.14  
    1.15 +val flatten = implode o map text_of;
    1.16 +
    1.17  fun is_regular (Token (_, (Error _, _))) = false
    1.18    | is_regular (Token (_, (EOF, _))) = false
    1.19    | is_regular _ = true;