# HG changeset patch
# User wenzelm
# Date 1516895427 -3600
# Node ID 524dc5c2a03173c6d33096984b82ef16ef23b87f
# Parent  189ab2c3026b9dfd15a8442d1f283be231dfeef1
allow cartouche within ML string;

diff -r 189ab2c3026b -r 524dc5c2a031 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 }