1.1 --- a/src/Pure/General/path.scala	Tue Jul 05 21:20:24 2011 +0200
     1.2 +++ b/src/Pure/General/path.scala	Tue Jul 05 21:32:48 2011 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4  
     1.5    def explode(str: String): Path =
     1.6    {
     1.7 -    val ss = Library.space_explode('/', str)
     1.8 +    val ss = space_explode('/', str)
     1.9      val r = ss.takeWhile(_.isEmpty).length
    1.10      val es = ss.dropWhile(_.isEmpty)
    1.11      val (roots, raw_elems) =
    1.12 @@ -94,7 +94,7 @@
    1.13    }
    1.14  
    1.15    def split(str: String): List[Path] =
    1.16 -    Library.space_explode(':', str).filter(_ != "").map(explode)
    1.17 +    space_explode(':', str).filterNot(_.isEmpty).map(explode)
    1.18  }
    1.19  
    1.20  

     2.1 --- a/src/Pure/System/isabelle_system.scala	Tue Jul 05 21:20:24 2011 +0200
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Tue Jul 05 21:32:48 2011 +0200
     2.3 @@ -96,7 +96,7 @@
     2.4          if (isabelle_symbols == "") error("Undefined environment variable: ISABELLE_SYMBOLS")
     2.5          val files =
     2.6            Path.split(isabelle_symbols).map(p => new File(standard_system.jvm_path(p.implode)))
     2.7 -        new Symbol.Interpretation(Standard_System.try_read(files).split("\n").toList)
     2.8 +        new Symbol.Interpretation(split_lines(Standard_System.try_read(files)))
     2.9        }
    2.10  
    2.11        _state = Some(State(standard_system, settings, symbols))

     3.1 --- a/src/Pure/System/standard_system.scala	Tue Jul 05 21:20:24 2011 +0200
     3.2 +++ b/src/Pure/System/standard_system.scala	Tue Jul 05 21:32:48 2011 +0200
     3.3 @@ -292,7 +292,7 @@
     3.4              path
     3.5            case path => path
     3.6          }
     3.7 -      for (p <- rest.split("/") if p != "") {
     3.8 +      for (p <- space_explode('/', rest) if p != "") {
     3.9          val len = result_path.length
    3.10          if (len > 0 && result_path(len - 1) != File.separatorChar)
    3.11            result_path += File.separatorChar

     4.1 --- a/src/Pure/library.scala	Tue Jul 05 21:20:24 2011 +0200
     4.2 +++ b/src/Pure/library.scala	Tue Jul 05 21:32:48 2011 +0200
     4.3 @@ -61,6 +61,8 @@
     4.4        result.toList
     4.5      }
     4.6  
     4.7 +  def split_lines(str: String): List[String] = space_explode('\n', str)
     4.8 +
     4.9  
    4.10    /* iterate over chunks (cf. space_explode) */
    4.11  
    4.12 @@ -185,13 +187,14 @@
    4.13  
    4.14  class Basic_Library
    4.15  {
    4.16 +  val ERROR = Library.ERROR
    4.17 +  val error = Library.error _
    4.18 +  val cat_error = Library.cat_error _
    4.19 +
    4.20    val space_explode = Library.space_explode _
    4.21 +  val split_lines = Library.split_lines _
    4.22  
    4.23    val quote = Library.quote _
    4.24    val commas = Library.commas _
    4.25    val commas_quote = Library.commas_quote _
    4.26 -
    4.27 -  val ERROR = Library.ERROR
    4.28 -  val error = Library.error _
    4.29 -  val cat_error = Library.cat_error _
    4.30  }

     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Jul 05 21:20:24 2011 +0200
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Jul 05 21:32:48 2011 +0200
     5.3 @@ -300,7 +300,7 @@
     5.4    def start_session()
     5.5    {
     5.6      val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
     5.7 -    val modes = Isabelle_System.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
     5.8 +    val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
     5.9      val logic = {
    5.10        val logic = Property("logic")
    5.11        if (logic != null && logic != "") logic