1.1 --- a/src/Pure/System/isabelle_system.ML	Thu Jun 30 14:51:32 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_system.ML	Thu Jun 30 14:55:01 2011 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  
     1.5  fun isabelle_tool name args =
     1.6    (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
     1.7 -      let val path = dir ^ "/" ^ name in
     1.8 +      let val path = File.platform_path (Path.append (Path.explode dir) (Path.basic name)) in
     1.9          if can OS.FileSys.modTime path andalso
    1.10            not (OS.FileSys.isDir path) andalso
    1.11            OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])

     2.1 --- a/src/Pure/System/isabelle_system.scala	Thu Jun 30 14:51:32 2011 +0200
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Jun 30 14:55:01 2011 +0200
     2.3 @@ -92,74 +92,19 @@
     2.4  
     2.5  
     2.6  
     2.7 -  /** file path specifications **/
     2.8 +  /** file-system operations **/
     2.9  
    2.10 -  /* expand_path */
    2.11 +  /* path specifications */
    2.12  
    2.13 -  private val Root = new Regex("(//+[^/]*|/)(.*)")
    2.14 -  private val Only_Root = new Regex("//+[^/]*|/")
    2.15 +  def standard_path(path: Path): String = path.expand(getenv_strict).implode
    2.16  
    2.17 -  def expand_path(isabelle_path: String): String =
    2.18 -  {
    2.19 -    val result_path = new StringBuilder
    2.20 -    def init(path: String): String =
    2.21 -    {
    2.22 -      path match {
    2.23 -        case Root(root, rest) =>
    2.24 -          result_path.clear
    2.25 -          result_path ++= root
    2.26 -          rest
    2.27 -        case _ => path
    2.28 -      }
    2.29 -    }
    2.30 -    def append(path: String)
    2.31 -    {
    2.32 -      val rest = init(path)
    2.33 -      for (p <- rest.split("/") if p != "" && p != ".") {
    2.34 -        if (p == "..") {
    2.35 -          val result = result_path.toString
    2.36 -          if (!Only_Root.pattern.matcher(result).matches) {
    2.37 -            val i = result.lastIndexOf("/")
    2.38 -            if (result == "")
    2.39 -              result_path ++= ".."
    2.40 -            else if (result.substring(i + 1) == "..")
    2.41 -              result_path ++= "/.."
    2.42 -            else if (i < 0)
    2.43 -              result_path.length = 0
    2.44 -            else
    2.45 -              result_path.length = i
    2.46 -          }
    2.47 -        }
    2.48 -        else {
    2.49 -          val len = result_path.length
    2.50 -          if (len > 0 && result_path(len - 1) != '/')
    2.51 -            result_path += '/'
    2.52 -          result_path ++= p
    2.53 -        }
    2.54 -      }
    2.55 -    }
    2.56 -    val rest = init(isabelle_path)
    2.57 -    for (p <- rest.split("/")) {
    2.58 -      if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
    2.59 -      else if (p == "~") append(getenv_strict("HOME"))
    2.60 -      else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
    2.61 -      else append(p)
    2.62 -    }
    2.63 -    result_path.toString
    2.64 -  }
    2.65 -
    2.66 -
    2.67 -  /* platform_path */
    2.68 -
    2.69 -  def platform_path(isabelle_path: String): String =
    2.70 -    jvm_path(expand_path(isabelle_path))
    2.71 -
    2.72 -  def platform_file(path: String) = new File(platform_path(path))
    2.73 +  def platform_path(path: Path): String = jvm_path(standard_path(path))
    2.74 +  def platform_file(path: Path) = new File(platform_path(path))
    2.75  
    2.76  
    2.77    /* try_read */
    2.78  
    2.79 -  def try_read(paths: Seq[String]): String =
    2.80 +  def try_read(paths: Seq[Path]): String =
    2.81    {
    2.82      val buf = new StringBuilder
    2.83      for {
    2.84 @@ -175,15 +120,15 @@
    2.85  
    2.86    private def try_file(file: File) = if (file.isFile) Some(file) else None
    2.87  
    2.88 -  def source_file(path: String): Option[File] =
    2.89 +  def source_file(path: Path): Option[File] =
    2.90    {
    2.91 -    if (path.startsWith("/") || path == "")
    2.92 +    if (path.is_absolute || path.is_current)
    2.93        try_file(platform_file(path))
    2.94      else {
    2.95 -      val pure_file = platform_file("$ISABELLE_HOME/src/Pure/" + path)
    2.96 +      val pure_file = platform_file(Path.explode("~~/src/Pure") + path)
    2.97        if (pure_file.isFile) Some(pure_file)
    2.98        else if (getenv("ML_SOURCES") != "")
    2.99 -        try_file(platform_file("$ML_SOURCES/" + path))
   2.100 +        try_file(platform_file(Path.explode("$ML_SOURCES") + path))
   2.101        else None
   2.102      }
   2.103    }
   2.104 @@ -208,7 +153,7 @@
   2.105    class Managed_Process(redirect: Boolean, args: String*)
   2.106    {
   2.107      private val params =
   2.108 -      List(expand_path("$ISABELLE_HOME/lib/scripts/process"), "group", "-", "no_script")
   2.109 +      List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
   2.110      private val proc = execute(redirect, (params ++ args):_*)
   2.111  
   2.112  
   2.113 @@ -295,7 +240,7 @@
   2.114    def isabelle_tool(name: String, args: String*): (String, Int) =
   2.115    {
   2.116      getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>
   2.117 -      val file = platform_file(dir + "/" + name)
   2.118 +      val file = platform_file(Path.explode(dir) + Path.basic(name))
   2.119        try {
   2.120          file.isFile && file.canRead && file.canExecute &&
   2.121            !name.endsWith("~") && !name.endsWith(".orig")
   2.122 @@ -303,8 +248,8 @@
   2.123        catch { case _: SecurityException => false }
   2.124      } match {
   2.125        case Some(dir) =>
   2.126 -        Standard_System.process_output(
   2.127 -          execute(true, (List(expand_path(dir + "/" + name)) ++ args): _*))
   2.128 +        val file = standard_path(Path.explode(dir) + Path.basic(name))
   2.129 +        Standard_System.process_output(execute(true, (List(file) ++ args): _*))
   2.130        case None => ("Unknown Isabelle tool: " + name, 2)
   2.131      }
   2.132    }
   2.133 @@ -336,7 +281,7 @@
   2.134    def fifo_input_stream(fifo: String): InputStream =
   2.135    {
   2.136      if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
   2.137 -      val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), fifo, "-")
   2.138 +      val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-")
   2.139        proc.getOutputStream.close
   2.140        proc.getErrorStream.close
   2.141        proc.getInputStream
   2.142 @@ -347,7 +292,7 @@
   2.143    def fifo_output_stream(fifo: String): OutputStream =
   2.144    {
   2.145      if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
   2.146 -      val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), "-", fifo)
   2.147 +      val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo)
   2.148        proc.getInputStream.close
   2.149        proc.getErrorStream.close
   2.150        val out = proc.getOutputStream
   2.151 @@ -379,7 +324,7 @@
   2.152      val ml_ident = getenv_strict("ML_IDENTIFIER")
   2.153      val logics = new mutable.ListBuffer[String]
   2.154      for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
   2.155 -      val files = platform_file(dir + "/" + ml_ident).listFiles()
   2.156 +      val files = platform_file(Path.explode(dir) + Path.explode(ml_ident)).listFiles()
   2.157        if (files != null) {
   2.158          for (file <- files if file.isFile) logics += file.getName
   2.159        }
   2.160 @@ -391,7 +336,8 @@
   2.161    /* symbols */
   2.162  
   2.163    val symbols = new Symbol.Interpretation(
   2.164 -    try_read(getenv_strict("ISABELLE_SYMBOLS").split(":").toList).split("\n").toList)
   2.165 +    try_read(getenv_strict("ISABELLE_SYMBOLS").split(":").toList.map(Path.explode))
   2.166 +      .split("\n").toList)
   2.167  
   2.168  
   2.169    /* fonts */
   2.170 @@ -403,6 +349,6 @@
   2.171    {
   2.172      val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
   2.173      for (font <- getenv_strict("ISABELLE_FONTS").split(":"))
   2.174 -      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font)))
   2.175 +      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(Path.explode(font))))
   2.176    }
   2.177  }

     3.1 --- a/src/Pure/System/session_manager.scala	Thu Jun 30 14:51:32 2011 +0200
     3.2 +++ b/src/Pure/System/session_manager.scala	Thu Jun 30 14:55:01 2011 +0200
     3.3 @@ -42,7 +42,7 @@
     3.4    def component_sessions(): List[List[String]] =
     3.5    {
     3.6      val toplevel_sessions =
     3.7 -      system.components().map(system.platform_file(_)).filter(is_session_dir)
     3.8 +      system.components().map(s => system.platform_file(Path.explode(s))).filter(is_session_dir)
     3.9      ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
    3.10    }
    3.11  }

     4.1 --- a/src/Tools/jEdit/src/html_panel.scala	Thu Jun 30 14:51:32 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Thu Jun 30 14:55:01 2011 +0200
     4.3 @@ -96,7 +96,7 @@
     4.4  <head>
     4.5  <style media="all" type="text/css">
     4.6  """ +
     4.7 -  system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
     4.8 +  system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
     4.9  
    4.10    private val template_tail =
    4.11  """

     5.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Jun 30 14:51:32 2011 +0200
     5.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Jun 30 14:55:01 2011 +0200
     5.3 @@ -28,7 +28,7 @@
     5.4    extends AbstractHyperlink(start, end, line, "")
     5.5  {
     5.6    override def click(view: View) = {
     5.7 -    Isabelle.system.source_file(def_file) match {
     5.8 +    Isabelle.system.source_file(Path.explode(def_file)) match {
     5.9        case None =>
    5.10          Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
    5.11        case Some(file) =>

     6.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Thu Jun 30 14:51:32 2011 +0200
     6.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Thu Jun 30 14:55:01 2011 +0200
     6.3 @@ -25,7 +25,7 @@
     6.4    /* main tabs */
     6.5  
     6.6    private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 14)
     6.7 -  readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
     6.8 +  readme.render_document(Isabelle.system.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
     6.9  
    6.10    private val syslog = new TextArea(Isabelle.session.syslog())
    6.11    syslog.editable = false