tuned;

--- 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)

--- 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)

--- 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)

--- 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

--- 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))
 

--- 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 */

--- 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

--- 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
   }

--- 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)

--- 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 :::