--- a/src/Pure/General/symbol.scala Thu Sep 22 00:12:17 2016 +0200
+++ b/src/Pure/General/symbol.scala Thu Sep 22 11:25:27 2016 +0200
@@ -64,9 +64,7 @@
/* symbol matching */
private val symbol_total = new Regex("""(?xs)
- [\ud800-\udbff][\udc00-\udfff] | \r\n |
- \\ < (?: \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* | \^? ([A-Za-z][A-Za-z0-9_']*)? ) >? |
- .""")
+ [\ud800-\udbff][\udc00-\udfff] | \r\n | \\ < \^? ([A-Za-z][A-Za-z0-9_']*)? >? | .""")
private def is_plain(c: Char): Boolean =
!(c == '\r' || c == '\\' || Character.isHighSurrogate(c))