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