tuned;
authorwenzelm
Fri Oct 27 11:46:03 2017 +0200 (19 months ago)
changeset 66923914935f8a462
parent 66922 5a476a87a535
child 66924 b4d4027f743b
tuned;
src/Pure/Admin/build_release.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/General/http.scala
src/Pure/General/long_name.scala
src/Pure/General/ssh.scala
src/Pure/PIDE/line.scala
src/Pure/PIDE/rendering.scala
src/Pure/System/numa.scala
src/Tools/jEdit/src/keymap_merge.scala
src/Tools/jEdit/src/scala_console.scala
     1.1 --- a/src/Pure/Admin/build_release.scala	Thu Oct 26 23:31:03 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_release.scala	Fri Oct 27 11:46:03 2017 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4          "W:" -> (arg => website = Some(Path.explode(arg))),
     1.5          "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
     1.6          "l" -> (_ => build_library = true),
     1.7 -        "p:" -> (arg => platform_families = Library.space_explode(',', arg)),
     1.8 +        "p:" -> (arg => platform_families = space_explode(',', arg)),
     1.9          "r:" -> (arg => rev = arg))
    1.10  
    1.11        val more_args = getopts(args)
     2.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 26 23:31:03 2017 +0200
     2.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Oct 27 11:46:03 2017 +0200
     2.3 @@ -343,7 +343,7 @@
     2.4            case Exn.Exn(exn) =>
     2.5              System.err.println("Exception trace for " + quote(task.name) + ":")
     2.6              exn.printStackTrace()
     2.7 -            val first_line = Library.split_lines(Exn.message(exn)).headOption getOrElse "exception"
     2.8 +            val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
     2.9              Some(first_line)
    2.10          }
    2.11        logger.log_end(end_date, err)
     3.1 --- a/src/Pure/General/http.scala	Thu Oct 26 23:31:03 2017 +0200
     3.2 +++ b/src/Pure/General/http.scala	Fri Oct 27 11:46:03 2017 +0200
     3.3 @@ -72,8 +72,8 @@
     3.4    sealed case class Arg(method: String, uri: URI, request: Bytes)
     3.5    {
     3.6      def decode_properties: Properties.T =
     3.7 -      Library.space_explode('&', request.text).map(s =>
     3.8 -        Library.space_explode('=', s) match {
     3.9 +      space_explode('&', request.text).map(s =>
    3.10 +        space_explode('=', s) match {
    3.11            case List(a, b) =>
    3.12              URLDecoder.decode(a, UTF8.charset_name) ->
    3.13              URLDecoder.decode(b, UTF8.charset_name)
     4.1 --- a/src/Pure/General/long_name.scala	Thu Oct 26 23:31:03 2017 +0200
     4.2 +++ b/src/Pure/General/long_name.scala	Fri Oct 27 11:46:03 2017 +0200
     4.3 @@ -15,7 +15,7 @@
     4.4    def is_qualified(name: String): Boolean = name.contains(separator_char)
     4.5  
     4.6    def implode(names: List[String]): String = names.mkString(separator)
     4.7 -  def explode(name: String): List[String] = Library.space_explode(separator_char, name)
     4.8 +  def explode(name: String): List[String] = space_explode(separator_char, name)
     4.9  
    4.10    def qualify(qual: String, name: String): String =
    4.11      if (qual == "" || name == "") name
     5.1 --- a/src/Pure/General/ssh.scala	Thu Oct 26 23:31:03 2017 +0200
     5.2 +++ b/src/Pure/General/ssh.scala	Fri Oct 27 11:46:03 2017 +0200
     5.3 @@ -63,7 +63,7 @@
     5.4      jsch.setKnownHosts(File.platform_path(known_hosts))
     5.5  
     5.6      val identity_files =
     5.7 -      Library.space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
     5.8 +      space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
     5.9      for (identity_file <- identity_files if identity_file.is_file)
    5.10        jsch.addIdentity(File.platform_path(identity_file))
    5.11  
     6.1 --- a/src/Pure/PIDE/line.scala	Thu Oct 26 23:31:03 2017 +0200
     6.2 +++ b/src/Pure/PIDE/line.scala	Fri Oct 27 11:46:03 2017 +0200
     6.3 @@ -18,7 +18,7 @@
     6.4      if (text.contains('\r')) text.replace("\r\n", "\n") else text
     6.5  
     6.6    def logical_lines(text: String): List[String] =
     6.7 -    Library.split_lines(normalize(text))
     6.8 +    split_lines(normalize(text))
     6.9  
    6.10  
    6.11    /* position */
     7.1 --- a/src/Pure/PIDE/rendering.scala	Thu Oct 26 23:31:03 2017 +0200
     7.2 +++ b/src/Pure/PIDE/rendering.scala	Fri Oct 27 11:46:03 2017 +0200
     7.3 @@ -306,7 +306,7 @@
     7.4          if (files == null) Nil
     7.5          else {
     7.6            val ignore =
     7.7 -            Library.space_explode(':', options.string("completion_path_ignore")).
     7.8 +            space_explode(':', options.string("completion_path_ignore")).
     7.9                map(s => FileSystems.getDefault.getPathMatcher("glob:" + s))
    7.10            (for {
    7.11              file <- files.iterator
     8.1 --- a/src/Pure/System/numa.scala	Thu Oct 26 23:31:03 2017 +0200
     8.2 +++ b/src/Pure/System/numa.scala	Fri Oct 27 11:46:03 2017 +0200
     8.3 @@ -26,7 +26,7 @@
     8.4        }
     8.5  
     8.6      if (numa_nodes_linux.is_file) {
     8.7 -      Library.space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
     8.8 +      space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
     8.9      }
    8.10      else Nil
    8.11    }
     9.1 --- a/src/Tools/jEdit/src/keymap_merge.scala	Thu Oct 26 23:31:03 2017 +0200
     9.2 +++ b/src/Tools/jEdit/src/keymap_merge.scala	Fri Oct 27 11:46:03 2017 +0200
     9.3 @@ -48,7 +48,7 @@
     9.4      private def prop_ignore: String = property + ".ignore"
     9.5  
     9.6      def ignored_keymaps(): List[String] =
     9.7 -      Library.space_explode(',', jEdit.getProperty(prop_ignore, ""))
     9.8 +      space_explode(',', jEdit.getProperty(prop_ignore, ""))
     9.9  
    9.10      def is_ignored(keymap_name: String): Boolean =
    9.11        ignored_keymaps().contains(keymap_name)
    10.1 --- a/src/Tools/jEdit/src/scala_console.scala	Thu Oct 26 23:31:03 2017 +0200
    10.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Fri Oct 27 11:46:03 2017 +0200
    10.3 @@ -34,7 +34,7 @@
    10.4        else Nil
    10.5  
    10.6      val initial_class_path =
    10.7 -      Library.space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
    10.8 +      space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
    10.9  
   10.10      val path =
   10.11        initial_class_path :::