src/Pure/ML/ml_lex.ML

--- a/src/Pure/ML/ml_lex.ML	Mon Aug 27 17:30:13 2018 +0200
+++ b/src/Pure/ML/ml_lex.ML	Mon Aug 27 19:12:48 2018 +0200
@@ -22,6 +22,7 @@
   val kind_of: token -> token_kind
   val content_of: token -> string
   val check_content_of: token -> string
+  val explode_content_of: bool -> token -> char list
   val flatten: token list -> string
   val source: (Symbol.symbol, 'a) Source.source ->
     (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
@@ -127,6 +128,10 @@
     Error msg => error msg
   | _ => content_of tok);
 
+fun explode_content_of SML =
+  check_content_of #>
+  (if SML then String.explode else Symbol.explode #> maps (Symbol.esc #> String.explode));
+
 
 (* flatten *)