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