src/Pure/ML/ml_lex.scala

--- a/src/Pure/ML/ml_lex.scala	Thu Jan 25 16:30:20 2018 +0100
+++ b/src/Pure/ML/ml_lex.scala	Thu Jan 25 16:50:27 2018 +0100
@@ -95,7 +95,8 @@
 
     private val str =
       one(character(c => c != '"' && c != '\\' && ' ' <= c && c <= '~')) |
-      one(s => Symbol.is_symbolic(s) | Symbol.is_control(s)) |
+      one(s =>
+        Symbol.is_open(s) || Symbol.is_close(s) || Symbol.is_symbolic(s) || Symbol.is_control(s)) |
       "\\" ~ escape ^^ { case x ~ y => x + y }