# HG changeset patch
# User wenzelm
# Date 1614805109 -3600
# Node ID ec52a1a6ed31f877637f5771efd912f91425238c
# Parent  79b120d1c1a398359d60017b53a9d1b408f691a0
tuned --- fewer warnings;

diff -r 79b120d1c1a3 -r ec52a1a6ed31 src/Pure/General/symbol.scala
--- 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))
diff -r 79b120d1c1a3 -r ec52a1a6ed31 src/Pure/library.scala
--- a/src/Pure/library.scala	Wed Mar 03 21:37:20 2021 +0100
+++ b/src/Pure/library.scala	Wed Mar 03 21:58:29 2021 +0100
@@ -148,7 +148,7 @@
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
   def strip_ansi_color(s: String): String =
-    s.replaceAll("""\u001b\[\d+m""", "")
+    s.replaceAll("\u001b\\[\\d+m", "")
 
 
   /* quote */