# HG changeset patch
# User wenzelm
# Date 1675697359 -3600
# Node ID 86217697863cb1540f27a1cab774d75b4826fe85
# Parent  e5ec449b4839e270e3a19ac87305617eda78dc62
tuned signature;

diff -r e5ec449b4839 -r 86217697863c src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Feb 06 16:26:40 2023 +0100
+++ b/src/Pure/General/file.scala	Mon Feb 06 16:29:19 2023 +0100
@@ -55,8 +55,7 @@
   /* symbolic path representation, e.g. "~~/src/Pure/ROOT.ML" */
 
   def symbolic_path(path: Path): String = {
-    val directories =
-      Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse
+    val directories = space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse
     val full_name = standard_path(path)
     directories.view.flatMap(a =>
       try {
diff -r e5ec449b4839 -r 86217697863c src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Mon Feb 06 16:26:40 2023 +0100
+++ b/src/Pure/General/mercurial.scala	Mon Feb 06 16:29:19 2023 +0100
@@ -248,7 +248,7 @@
 
     def tags(rev: String = "tip"): String = {
       val result = identify(rev, options = "-t")
-      Library.space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
+      space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
     }
 
     def paths(args: String = "", options: String = ""): List[String] =
diff -r e5ec449b4839 -r 86217697863c src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Mon Feb 06 16:26:40 2023 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Mon Feb 06 16:29:19 2023 +0100
@@ -54,7 +54,7 @@
     consume: Properties.T => Unit = Console.println
   ): Unit = {
     def progress_stdout(line: String): Unit = {
-      val props = Library.space_explode(',', line).flatMap(Properties.Eq.unapply)
+      val props = space_explode(',', line).flatMap(Properties.Eq.unapply)
       if (props.nonEmpty) consume(props)
     }
 
diff -r e5ec449b4839 -r 86217697863c src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Feb 06 16:26:40 2023 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Feb 06 16:29:19 2023 +0100
@@ -510,8 +510,7 @@
   def open_external_file(name: String): Boolean = {
     val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
     val external =
-      ext.nonEmpty &&
-      Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
+      ext.nonEmpty && space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
     if (external) {
       if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
       else open(name)
diff -r e5ec449b4839 -r 86217697863c src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Mon Feb 06 16:26:40 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Mon Feb 06 16:29:19 2023 +0100
@@ -703,7 +703,7 @@
   /* cite commands */
 
   def cite_commands(options: Options): List[String] =
-    Library.space_explode(',', options.string("document_cite_commands"))
+    space_explode(',', options.string("document_cite_commands"))
 
   val CITE = "cite"
   val NOCITE = "nocite"
@@ -828,7 +828,7 @@
       val location =
         if (loc.startsWith("[") && loc.endsWith("]")) loc.substring(1, loc.length - 1)
         else loc
-      val citations = Library.space_explode(',', m.group(3)).map(_.trim)
+      val citations = space_explode(',', m.group(3)).map(_.trim)
       Regex.quoteReplacement(cite_antiquotation(name, location, citations))
     })
 
diff -r e5ec449b4839 -r 86217697863c src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon Feb 06 16:26:40 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Mon Feb 06 16:29:19 2023 +0100
@@ -19,7 +19,7 @@
 
   object Document_Variant {
     def parse(opt: String): Document_Variant =
-      Library.space_explode('=', opt) match {
+      space_explode('=', opt) match {
         case List(name) => Document_Variant(name, Latex.Tags.empty)
         case List(name, tags) => Document_Variant(name, Latex.Tags(tags))
         case _ => error("Malformed document variant: " + quote(opt))
diff -r e5ec449b4839 -r 86217697863c src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Mon Feb 06 16:26:40 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Mon Feb 06 16:29:19 2023 +0100
@@ -99,8 +99,7 @@
 
     val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant"
 
-    private def explode(spec: String): List[String] =
-      Library.space_explode(',', spec)
+    private def explode(spec: String): List[String] = space_explode(',', spec)
 
     def apply(spec: String): Tags =
       new Tags(spec,
diff -r e5ec449b4839 -r 86217697863c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Feb 06 16:26:40 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Feb 06 16:29:19 2023 +0100
@@ -689,7 +689,7 @@
 
     def document_variants: List[Document_Build.Document_Variant] = {
       val variants =
-        Library.space_explode(':', options.string("document_variants")).
+        space_explode(':', options.string("document_variants")).
           map(Document_Build.Document_Variant.parse)
 
       val dups = Library.duplicates(variants.map(_.name))
diff -r e5ec449b4839 -r 86217697863c src/Pure/Tools/dotnet_setup.scala
--- a/src/Pure/Tools/dotnet_setup.scala	Mon Feb 06 16:26:40 2023 +0100
+++ b/src/Pure/Tools/dotnet_setup.scala	Mon Feb 06 16:29:19 2023 +0100
@@ -186,7 +186,7 @@
           "V:" -> (arg => version = arg),
           "f" -> (_ => force = true),
           "n" -> (_ => dry_run = true),
-          "p:" -> (arg => platforms = Library.space_explode(',', arg).map(check_platform_spec)),
+          "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform_spec)),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
diff -r e5ec449b4839 -r 86217697863c src/Tools/VSCode/src/build_vscodium.scala
--- a/src/Tools/VSCode/src/build_vscodium.scala	Mon Feb 06 16:26:40 2023 +0100
+++ b/src/Tools/VSCode/src/build_vscodium.scala	Mon Feb 06 16:29:19 2023 +0100
@@ -426,7 +426,7 @@
   for targeting Windows.
 """,
           "D:" -> (arg => target_dir = Path.explode(arg)),
-          "p:" -> (arg => platforms = Library.space_explode(',', arg).map(Platform.Family.parse)),
+          "p:" -> (arg => platforms = space_explode(',', arg).map(Platform.Family.parse)),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)