# HG changeset patch
# User wenzelm
# Date 1761242954 -7200
# Node ID 0e2e5adbdea5706a51c20f59ab0605199ea76cf1
# Parent  6a097e8add88aeedb2d7dc32f7352663a01dfff0
tuned: prefer high-level operation;

diff -r 6a097e8add88 -r 0e2e5adbdea5 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Oct 23 18:00:28 2025 +0200
+++ b/src/Pure/General/symbol.scala	Thu Oct 23 20:09:14 2025 +0200
@@ -393,7 +393,7 @@
             case _ => err()
           }
         }
-        decl.split("\\s+").toList match {
+        Word.explode(decl) match {
           case sym :: props if sym.length > 1 && !is_malformed(sym) =>
             (sym, read_props(props))
           case _ => err()
diff -r 6a097e8add88 -r 0e2e5adbdea5 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Thu Oct 23 18:00:28 2025 +0200
+++ b/src/Pure/System/components.scala	Thu Oct 23 20:09:14 2025 +0200
@@ -225,7 +225,7 @@
             for (case (a, b) <- File.read_props(props_path).asScala.toList)
               yield {
                 if (!default_platforms.defined(a)) error("Bad platform family " + quote(a))
-                val ps = List.from(b.split("\\s+").iterator.filter(_.nonEmpty)).map(Path.explode)
+                val ps = Word.explode(b).map(Path.explode)
                 for (p <- ps if !p.all_basic) error("Bad path outside component " + p)
                 a -> ps
               }
diff -r 6a097e8add88 -r 0e2e5adbdea5 src/Tools/VSCode/src/vscode_sledgehammer.scala
--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Thu Oct 23 18:00:28 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Thu Oct 23 20:09:14 2025 +0200
@@ -48,8 +48,8 @@
   }
 
   def handle_request(provers: String, isar: Boolean, try0: Boolean, purpose: Int): Unit = {
-    val available_provers = persistent_options.string("sledgehammer_provers").split("\\s+").toSet
-    val user_provers = provers.trim.split("\\s+").toSet
+    val available_provers = Word.explode(persistent_options.string("sledgehammer_provers")).toSet
+    val user_provers = Word.explode(provers).toSet
     val invalid = user_provers.diff(available_provers)
     if (invalid.nonEmpty) {
       server.channel.write(LSP.Sledgehammer_NoProver_Response.apply(invalid.toList))