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)))
   }
 }