# HG changeset patch
# User wenzelm
# Date 1309894368 -7200
# Node ID 7f933761764bf75a8b9f340b36792741528c4d4d
# Parent  9d34288e93516f9d120b115b6822030d2a207171
prefer space_explode/split_lines as in Isabelle/ML;

diff -r 9d34288e9351 -r 7f933761764b src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Tue Jul 05 21:20:24 2011 +0200
+++ b/src/Pure/General/path.scala	Tue Jul 05 21:32:48 2011 +0200
@@ -82,7 +82,7 @@
 
   def explode(str: String): Path =
   {
-    val ss = Library.space_explode('/', str)
+    val ss = space_explode('/', str)
     val r = ss.takeWhile(_.isEmpty).length
     val es = ss.dropWhile(_.isEmpty)
     val (roots, raw_elems) =
@@ -94,7 +94,7 @@
   }
 
   def split(str: String): List[Path] =
-    Library.space_explode(':', str).filter(_ != "").map(explode)
+    space_explode(':', str).filterNot(_.isEmpty).map(explode)
 }
 
 
diff -r 9d34288e9351 -r 7f933761764b src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Jul 05 21:20:24 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Jul 05 21:32:48 2011 +0200
@@ -96,7 +96,7 @@
         if (isabelle_symbols == "") error("Undefined environment variable: ISABELLE_SYMBOLS")
         val files =
           Path.split(isabelle_symbols).map(p => new File(standard_system.jvm_path(p.implode)))
-        new Symbol.Interpretation(Standard_System.try_read(files).split("\n").toList)
+        new Symbol.Interpretation(split_lines(Standard_System.try_read(files)))
       }
 
       _state = Some(State(standard_system, settings, symbols))
diff -r 9d34288e9351 -r 7f933761764b src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Tue Jul 05 21:20:24 2011 +0200
+++ b/src/Pure/System/standard_system.scala	Tue Jul 05 21:32:48 2011 +0200
@@ -292,7 +292,7 @@
             path
           case path => path
         }
-      for (p <- rest.split("/") if p != "") {
+      for (p <- space_explode('/', rest) if p != "") {
         val len = result_path.length
         if (len > 0 && result_path(len - 1) != File.separatorChar)
           result_path += File.separatorChar
diff -r 9d34288e9351 -r 7f933761764b src/Pure/library.scala
--- a/src/Pure/library.scala	Tue Jul 05 21:20:24 2011 +0200
+++ b/src/Pure/library.scala	Tue Jul 05 21:32:48 2011 +0200
@@ -61,6 +61,8 @@
       result.toList
     }
 
+  def split_lines(str: String): List[String] = space_explode('\n', str)
+
 
   /* iterate over chunks (cf. space_explode) */
 
@@ -185,13 +187,14 @@
 
 class Basic_Library
 {
+  val ERROR = Library.ERROR
+  val error = Library.error _
+  val cat_error = Library.cat_error _
+
   val space_explode = Library.space_explode _
+  val split_lines = Library.split_lines _
 
   val quote = Library.quote _
   val commas = Library.commas _
   val commas_quote = Library.commas_quote _
-
-  val ERROR = Library.ERROR
-  val error = Library.error _
-  val cat_error = Library.cat_error _
 }
diff -r 9d34288e9351 -r 7f933761764b src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Jul 05 21:20:24 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Jul 05 21:32:48 2011 +0200
@@ -300,7 +300,7 @@
   def start_session()
   {
     val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
-    val modes = Isabelle_System.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
+    val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
     val logic = {
       val logic = Property("logic")
       if (logic != null && logic != "") logic