Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned --- fewer warnings;
authorwenzelm
Wed, 03 Mar 2021 21:58:29 +0100
changeset 73355 ec52a1a6ed31
parent 73354 79b120d1c1a3
child 73356 819f6033fb4e
tuned --- fewer warnings;
src/Pure/General/symbol.scala file | annotate | diff | comparison | revisions
src/Pure/library.scala file | annotate | diff | comparison | revisions 
--- 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))
--- 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 */
isabelle