1.1 --- a/src/Pure/General/path.scala	Tue Jul 05 20:36:49 2011 +0200
     1.2 +++ b/src/Pure/General/path.scala	Tue Jul 05 21:20:24 2011 +0200
     1.3 @@ -92,8 +92,12 @@
     1.4        else (List(root_elem(es.head)), es.tail)
     1.5      Path(norm_elems(explode_elems(raw_elems) ++ roots))
     1.6    }
     1.7 +
     1.8 +  def split(str: String): List[Path] =
     1.9 +    Library.space_explode(':', str).filter(_ != "").map(explode)
    1.10  }
    1.11  
    1.12 +
    1.13  class Path
    1.14  {
    1.15    protected val elems: List[Path.Elem] = Nil   // reversed elements

     2.1 --- a/src/Pure/System/isabelle_system.scala	Tue Jul 05 20:36:49 2011 +0200
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Tue Jul 05 21:20:24 2011 +0200
     2.3 @@ -95,7 +95,7 @@
     2.4          val isabelle_symbols = settings.getOrElse("ISABELLE_SYMBOLS", "")
     2.5          if (isabelle_symbols == "") error("Undefined environment variable: ISABELLE_SYMBOLS")
     2.6          val files =
     2.7 -          isabelle_symbols.split(":").toList.map(s => new File(standard_system.jvm_path(s)))
     2.8 +          Path.split(isabelle_symbols).map(p => new File(standard_system.jvm_path(p.implode)))
     2.9          new Symbol.Interpretation(Standard_System.try_read(files).split("\n").toList)
    2.10        }
    2.11  
    2.12 @@ -265,8 +265,8 @@
    2.13  
    2.14    def isabelle_tool(name: String, args: String*): (String, Int) =
    2.15    {
    2.16 -    getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>
    2.17 -      val file = platform_file(Path.explode(dir) + Path.basic(name))
    2.18 +    Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
    2.19 +      val file = platform_file(dir + Path.basic(name))
    2.20        try {
    2.21          file.isFile && file.canRead && file.canExecute &&
    2.22            !name.endsWith("~") && !name.endsWith(".orig")
    2.23 @@ -274,7 +274,7 @@
    2.24        catch { case _: SecurityException => false }
    2.25      } match {
    2.26        case Some(dir) =>
    2.27 -        val file = standard_path(Path.explode(dir) + Path.basic(name))
    2.28 +        val file = standard_path(dir + Path.basic(name))
    2.29          Standard_System.process_output(execute(true, (List(file) ++ args): _*))
    2.30        case None => ("Unknown Isabelle tool: " + name, 2)
    2.31      }
    2.32 @@ -334,8 +334,8 @@
    2.33  
    2.34    /* components */
    2.35  
    2.36 -  def components(): List[String] =
    2.37 -    getenv_strict("ISABELLE_COMPONENTS").split(":").toList
    2.38 +  def components(): List[Path] =
    2.39 +    Path.split(getenv_strict("ISABELLE_COMPONENTS"))
    2.40  
    2.41  
    2.42    /* find logics */
    2.43 @@ -344,8 +344,8 @@
    2.44    {
    2.45      val ml_ident = getenv_strict("ML_IDENTIFIER")
    2.46      val logics = new mutable.ListBuffer[String]
    2.47 -    for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
    2.48 -      val files = platform_file(Path.explode(dir) + Path.explode(ml_ident)).listFiles()
    2.49 +    for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) {
    2.50 +      val files = platform_file(dir + Path.explode(ml_ident)).listFiles()
    2.51        if (files != null) {
    2.52          for (file <- files if file.isFile) logics += file.getName
    2.53        }
    2.54 @@ -362,7 +362,7 @@
    2.55    def install_fonts()
    2.56    {
    2.57      val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
    2.58 -    for (font <- getenv_strict("ISABELLE_FONTS").split(":"))
    2.59 -      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(Path.explode(font))))
    2.60 +    for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
    2.61 +      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font)))
    2.62    }
    2.63  }

     3.1 --- a/src/Pure/System/session_manager.scala	Tue Jul 05 20:36:49 2011 +0200
     3.2 +++ b/src/Pure/System/session_manager.scala	Tue Jul 05 21:20:24 2011 +0200
     3.3 @@ -42,8 +42,7 @@
     3.4    def component_sessions(): List[List[String]] =
     3.5    {
     3.6      val toplevel_sessions =
     3.7 -      Isabelle_System.components().map(s =>
     3.8 -        Isabelle_System.platform_file(Path.explode(s))).filter(is_session_dir)
     3.9 +      Isabelle_System.components().map(Isabelle_System.platform_file).filter(is_session_dir)
    3.10      ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
    3.11    }
    3.12  }

     4.1 --- a/src/Tools/jEdit/src/html_panel.scala	Tue Jul 05 20:36:49 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Tue Jul 05 21:20:24 2011 +0200
     4.3 @@ -92,8 +92,7 @@
     4.4  <head>
     4.5  <style media="all" type="text/css">
     4.6  """ +
     4.7 -  Isabelle_System.try_read(
     4.8 -    Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
     4.9 +  Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS")))
    4.10  
    4.11    private val template_tail =
    4.12  """