# HG changeset patch
# User wenzelm
# Date 1509097563 -7200
# Node ID 914935f8a462515c86a10e706e00a56b166316aa
# Parent  5a476a87a535ee0e09dcb68a096687dadaec9d0c
tuned;

diff -r 5a476a87a535 -r 914935f8a462 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Thu Oct 26 23:31:03 2017 +0200
+++ b/src/Pure/Admin/build_release.scala	Fri Oct 27 11:46:03 2017 +0200
@@ -223,7 +223,7 @@
         "W:" -> (arg => website = Some(Path.explode(arg))),
         "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
         "l" -> (_ => build_library = true),
-        "p:" -> (arg => platform_families = Library.space_explode(',', arg)),
+        "p:" -> (arg => platform_families = space_explode(',', arg)),
         "r:" -> (arg => rev = arg))
 
       val more_args = getopts(args)
diff -r 5a476a87a535 -r 914935f8a462 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 26 23:31:03 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Oct 27 11:46:03 2017 +0200
@@ -343,7 +343,7 @@
           case Exn.Exn(exn) =>
             System.err.println("Exception trace for " + quote(task.name) + ":")
             exn.printStackTrace()
-            val first_line = Library.split_lines(Exn.message(exn)).headOption getOrElse "exception"
+            val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
             Some(first_line)
         }
       logger.log_end(end_date, err)
diff -r 5a476a87a535 -r 914935f8a462 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Oct 26 23:31:03 2017 +0200
+++ b/src/Pure/General/http.scala	Fri Oct 27 11:46:03 2017 +0200
@@ -72,8 +72,8 @@
   sealed case class Arg(method: String, uri: URI, request: Bytes)
   {
     def decode_properties: Properties.T =
-      Library.space_explode('&', request.text).map(s =>
-        Library.space_explode('=', s) match {
+      space_explode('&', request.text).map(s =>
+        space_explode('=', s) match {
           case List(a, b) =>
             URLDecoder.decode(a, UTF8.charset_name) ->
             URLDecoder.decode(b, UTF8.charset_name)
diff -r 5a476a87a535 -r 914935f8a462 src/Pure/General/long_name.scala
--- a/src/Pure/General/long_name.scala	Thu Oct 26 23:31:03 2017 +0200
+++ b/src/Pure/General/long_name.scala	Fri Oct 27 11:46:03 2017 +0200
@@ -15,7 +15,7 @@
   def is_qualified(name: String): Boolean = name.contains(separator_char)
 
   def implode(names: List[String]): String = names.mkString(separator)
-  def explode(name: String): List[String] = Library.space_explode(separator_char, name)
+  def explode(name: String): List[String] = space_explode(separator_char, name)
 
   def qualify(qual: String, name: String): String =
     if (qual == "" || name == "") name
diff -r 5a476a87a535 -r 914935f8a462 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu Oct 26 23:31:03 2017 +0200
+++ b/src/Pure/General/ssh.scala	Fri Oct 27 11:46:03 2017 +0200
@@ -63,7 +63,7 @@
     jsch.setKnownHosts(File.platform_path(known_hosts))
 
     val identity_files =
-      Library.space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
+      space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
     for (identity_file <- identity_files if identity_file.is_file)
       jsch.addIdentity(File.platform_path(identity_file))
 
diff -r 5a476a87a535 -r 914935f8a462 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Thu Oct 26 23:31:03 2017 +0200
+++ b/src/Pure/PIDE/line.scala	Fri Oct 27 11:46:03 2017 +0200
@@ -18,7 +18,7 @@
     if (text.contains('\r')) text.replace("\r\n", "\n") else text
 
   def logical_lines(text: String): List[String] =
-    Library.split_lines(normalize(text))
+    split_lines(normalize(text))
 
 
   /* position */
diff -r 5a476a87a535 -r 914935f8a462 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Thu Oct 26 23:31:03 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala	Fri Oct 27 11:46:03 2017 +0200
@@ -306,7 +306,7 @@
         if (files == null) Nil
         else {
           val ignore =
-            Library.space_explode(':', options.string("completion_path_ignore")).
+            space_explode(':', options.string("completion_path_ignore")).
               map(s => FileSystems.getDefault.getPathMatcher("glob:" + s))
           (for {
             file <- files.iterator
diff -r 5a476a87a535 -r 914935f8a462 src/Pure/System/numa.scala
--- a/src/Pure/System/numa.scala	Thu Oct 26 23:31:03 2017 +0200
+++ b/src/Pure/System/numa.scala	Fri Oct 27 11:46:03 2017 +0200
@@ -26,7 +26,7 @@
       }
 
     if (numa_nodes_linux.is_file) {
-      Library.space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
+      space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
     }
     else Nil
   }
diff -r 5a476a87a535 -r 914935f8a462 src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Thu Oct 26 23:31:03 2017 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Fri Oct 27 11:46:03 2017 +0200
@@ -48,7 +48,7 @@
     private def prop_ignore: String = property + ".ignore"
 
     def ignored_keymaps(): List[String] =
-      Library.space_explode(',', jEdit.getProperty(prop_ignore, ""))
+      space_explode(',', jEdit.getProperty(prop_ignore, ""))
 
     def is_ignored(keymap_name: String): Boolean =
       ignored_keymaps().contains(keymap_name)
diff -r 5a476a87a535 -r 914935f8a462 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Thu Oct 26 23:31:03 2017 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri Oct 27 11:46:03 2017 +0200
@@ -34,7 +34,7 @@
       else Nil
 
     val initial_class_path =
-      Library.space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
+      space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
 
     val path =
       initial_class_path :::