# HG changeset patch
# User wenzelm
# Date 1309893624 -7200
# Node ID 9d34288e93516f9d120b115b6822030d2a207171
# Parent  aad4f1956098ebe74200587fb29a9d5029eb7314
Path.split convenience;

diff -r aad4f1956098 -r 9d34288e9351 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Tue Jul 05 20:36:49 2011 +0200
+++ b/src/Pure/General/path.scala	Tue Jul 05 21:20:24 2011 +0200
@@ -92,8 +92,12 @@
       else (List(root_elem(es.head)), es.tail)
     Path(norm_elems(explode_elems(raw_elems) ++ roots))
   }
+
+  def split(str: String): List[Path] =
+    Library.space_explode(':', str).filter(_ != "").map(explode)
 }
 
+
 class Path
 {
   protected val elems: List[Path.Elem] = Nil   // reversed elements
diff -r aad4f1956098 -r 9d34288e9351 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Jul 05 20:36:49 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Jul 05 21:20:24 2011 +0200
@@ -95,7 +95,7 @@
         val isabelle_symbols = settings.getOrElse("ISABELLE_SYMBOLS", "")
         if (isabelle_symbols == "") error("Undefined environment variable: ISABELLE_SYMBOLS")
         val files =
-          isabelle_symbols.split(":").toList.map(s => new File(standard_system.jvm_path(s)))
+          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)
       }
 
@@ -265,8 +265,8 @@
 
   def isabelle_tool(name: String, args: String*): (String, Int) =
   {
-    getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>
-      val file = platform_file(Path.explode(dir) + Path.basic(name))
+    Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
+      val file = platform_file(dir + Path.basic(name))
       try {
         file.isFile && file.canRead && file.canExecute &&
           !name.endsWith("~") && !name.endsWith(".orig")
@@ -274,7 +274,7 @@
       catch { case _: SecurityException => false }
     } match {
       case Some(dir) =>
-        val file = standard_path(Path.explode(dir) + Path.basic(name))
+        val file = standard_path(dir + Path.basic(name))
         Standard_System.process_output(execute(true, (List(file) ++ args): _*))
       case None => ("Unknown Isabelle tool: " + name, 2)
     }
@@ -334,8 +334,8 @@
 
   /* components */
 
-  def components(): List[String] =
-    getenv_strict("ISABELLE_COMPONENTS").split(":").toList
+  def components(): List[Path] =
+    Path.split(getenv_strict("ISABELLE_COMPONENTS"))
 
 
   /* find logics */
@@ -344,8 +344,8 @@
   {
     val ml_ident = getenv_strict("ML_IDENTIFIER")
     val logics = new mutable.ListBuffer[String]
-    for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
-      val files = platform_file(Path.explode(dir) + Path.explode(ml_ident)).listFiles()
+    for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) {
+      val files = platform_file(dir + Path.explode(ml_ident)).listFiles()
       if (files != null) {
         for (file <- files if file.isFile) logics += file.getName
       }
@@ -362,7 +362,7 @@
   def install_fonts()
   {
     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
-    for (font <- getenv_strict("ISABELLE_FONTS").split(":"))
-      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(Path.explode(font))))
+    for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
+      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font)))
   }
 }
diff -r aad4f1956098 -r 9d34288e9351 src/Pure/System/session_manager.scala
--- a/src/Pure/System/session_manager.scala	Tue Jul 05 20:36:49 2011 +0200
+++ b/src/Pure/System/session_manager.scala	Tue Jul 05 21:20:24 2011 +0200
@@ -42,8 +42,7 @@
   def component_sessions(): List[List[String]] =
   {
     val toplevel_sessions =
-      Isabelle_System.components().map(s =>
-        Isabelle_System.platform_file(Path.explode(s))).filter(is_session_dir)
+      Isabelle_System.components().map(Isabelle_System.platform_file).filter(is_session_dir)
     ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
   }
 }
diff -r aad4f1956098 -r 9d34288e9351 src/Tools/jEdit/src/html_panel.scala
--- a/src/Tools/jEdit/src/html_panel.scala	Tue Jul 05 20:36:49 2011 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala	Tue Jul 05 21:20:24 2011 +0200
@@ -92,8 +92,7 @@
 <head>
 <style media="all" type="text/css">
 """ +
-  Isabelle_System.try_read(
-    Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
+  Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS")))
 
   private val template_tail =
 """