src/Pure/General/symbol.scala
changeset 73602 ec52a1a6ed31
parent 73587 0af9e7e4476f
child 73606 d8a0e996614b
--- a/src/Pure/General/symbol.scala	Wed Mar 03 21:37:20 2021 +0100
+++ b/src/Pure/General/symbol.scala	Wed Mar 03 21:58:29 2021 +0100
@@ -70,8 +70,9 @@
 
   /* symbol matching */
 
-  private val symbol_total = new Regex("""(?xs)
-    [\ud800-\udbff][\udc00-\udfff] | \r\n | \\ < \^? ([A-Za-z][A-Za-z0-9_']*)? >? | .""")
+  private val symbol_total =
+    new Regex("(?xs) [\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))