author | wenzelm |
Thu, 25 Jan 2018 16:50:27 +0100 | |
changeset 67509 | 524dc5c2a031 |
parent 67508 | 189ab2c3026b |
child 67510 | 9624711ef2de |
--- 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 }