# HG changeset patch
# User wenzelm
# Date 1392479748 -3600
# Node ID 72238ea2201cbca42c9ef4b9ddd9d0471f6fe27c
# Parent  fdde1d62e1fb6805fd89314097cad0a37cc880bd
clarified Isabelle/ML strings;

diff -r fdde1d62e1fb -r 72238ea2201c src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Sat Feb 15 16:49:10 2014 +0100
+++ b/src/Pure/ML/ml_lex.scala	Sat Feb 15 16:55:48 2014 +0100
@@ -68,6 +68,7 @@
       repeated(character(Symbol.is_ascii_digit), 3, 3)
 
     private val str =
+      one(Symbol.is_symbolic) |
       one(character(c => c != '"' && c != '\\' && ' ' <= c && c <= '~')) |
       "\\" ~ escape ^^ { case x ~ y => x + y }