allow cartouche within ML string;
authorwenzelm
Thu, 25 Jan 2018 16:50:27 +0100
changeset 67509 524dc5c2a031
parent 67508 189ab2c3026b
child 67510 9624711ef2de
allow cartouche within ML string;
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 }