# HG changeset patch
# User wenzelm
# Date 1662734683 -7200
# Node ID bcca0fbb8a34dc10fc2fdb9c2cedd4f577a970c9
# Parent  c6c0947804d68307511736e5a17054ed11f440a7
tuned: prefer Scala Regex operations;

diff -r c6c0947804d6 -r bcca0fbb8a34 src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Fri Sep 09 14:47:42 2022 +0200
+++ b/src/Pure/Admin/build_jdk.scala	Fri Sep 09 16:44:43 2022 +0200
@@ -41,7 +41,7 @@
       val path = jdk_dir + Path.explode("bin") + Path.explode(exe)
       if (path.is_file) {
         val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out
-        if (platform_regex.pattern.matcher(file_descr).matches) {
+        if (platform_regex.matches(file_descr)) {
           val Version = ("^(" + major_version + """[0-9.+]+)(?:-LTS)?$""").r
           val version_lines =
             Isabelle_System.bash("strings " + File.bash_path(path)).check
diff -r c6c0947804d6 -r bcca0fbb8a34 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Fri Sep 09 14:47:42 2022 +0200
+++ b/src/Pure/General/completion.scala	Fri Sep 09 16:44:43 2022 +0200
@@ -252,7 +252,7 @@
     override val whiteSpace = "".r
 
     private val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>?)""".r
-    def is_symboloid(s: CharSequence): Boolean = symboloid_regex.pattern.matcher(s).matches
+    def is_symboloid(s: CharSequence): Boolean = symboloid_regex.matches(s)
 
     private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
     private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
@@ -262,7 +262,7 @@
     private def word2: Parser[String] = "[a-zA-Z0-9_'.]{2,}".r
     private def underscores: Parser[String] = "_*".r
 
-    def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
+    def is_word(s: CharSequence): Boolean = word_regex.matches(s)
     def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
 
     def read_symbol(in: CharSequence): Option[String] = {
diff -r c6c0947804d6 -r bcca0fbb8a34 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Sep 09 14:47:42 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Sep 09 16:44:43 2022 +0200
@@ -173,8 +173,7 @@
 
   def make_matcher(pats: List[String]): Entry_Name => Boolean = {
     val regs = pats.map(make_regex)
-    (entry_name: Entry_Name) =>
-      regs.exists(_.pattern.matcher(entry_name.compound_name).matches)
+    (entry_name: Entry_Name) => regs.exists(_.matches(entry_name.compound_name))
   }
 
   def make_entry(
diff -r c6c0947804d6 -r bcca0fbb8a34 src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala	Fri Sep 09 14:47:42 2022 +0200
+++ b/src/Tools/Graphview/tree_panel.scala	Fri Sep 09 16:44:43 2022 +0200
@@ -97,7 +97,7 @@
   private def selection_filter(node: Graph_Display.Node): Boolean =
     selection_pattern match {
       case None => false
-      case Some(re) => re.pattern.matcher(node.toString).find
+      case Some(re) => re.findFirstIn(node.toString).isDefined
     }
 
   private val selection_label = new Label("Selection:") {