# HG changeset patch
# User wenzelm
# Date 1246121168 -7200
# Node ID 8199c9a42941fe9678d5c64129c07ae344daff15
# Parent  2c0ab4485f488432c1f4acd87352d457e95c3c84
added isabelle_path;
tuned platform_path;
tuned comments;

diff -r 2c0ab4485f48 -r 8199c9a42941 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Jun 27 17:35:08 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Jun 27 18:46:08 2009 +0200
@@ -7,6 +7,7 @@
 package isabelle
 
 import java.util.regex.Pattern
+import java.util.Locale
 import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException}
 
 import scala.io.Source
@@ -129,9 +130,9 @@
 
   /** file path specifications **/
 
-  /* Isabelle paths */
+  /* expand_path */
 
-  def expand_path(source_path: String): String =
+  def expand_path(isabelle_path: String): String =
   {
     val result_path = new StringBuilder
     def init(path: String)
@@ -165,8 +166,8 @@
         }
       }
     }
-    init(source_path)
-    for (p <- source_path.split("/")) {
+    init(isabelle_path)
+    for (p <- isabelle_path.split("/")) {
       if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
       else if (p == "~") append(getenv_strict("HOME"))
       else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
@@ -176,18 +177,17 @@
   }
 
 
-  /* platform paths */
+  /* platform_path */
 
-  private val Cygdrive = new Regex(
-    if (drive_prefix == "") "\0"
-    else Pattern.quote(drive_prefix) + "/([a-zA-Z])($|/.*)")
+  private val Cygdrive =
+    new Regex(Pattern.quote(drive_prefix) + "/([a-zA-Z])($|/.*)")
 
-  def platform_path(source_path: String): String =
+  def platform_path(isabelle_path: String): String =
   {
     val result_path = new StringBuilder
     val rest =
-      expand_path(source_path) match {
-        case Cygdrive(drive, rest) =>
+      expand_path(isabelle_path) match {
+        case Cygdrive(drive, rest) if Isabelle_System.is_cygwin =>
           result_path ++= (drive + ":" + File.separator)
           rest
         case path if path.startsWith("/") =>
@@ -207,6 +207,27 @@
   def platform_file(path: String) = new File(platform_path(path))
 
 
+  /* isabelle_path */
+
+  private val Platform_Root = new Regex("(?i)" +
+    Pattern.quote(platform_root) + """(?:\\|\z)(.*)""")
+  private val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
+
+  def isabelle_path(platform_path: String): String =
+  {
+    if (Isabelle_System.is_cygwin) {
+      platform_path.replace('/', '\\') match {
+        case Platform_Root(rest) => "/" + rest.replace('\\', '/')
+        case Drive(letter, rest) =>
+          drive_prefix + "/" + letter.toLowerCase(Locale.ENGLISH) +
+            (if (rest == "") "" else "/" + rest.replace('\\', '/'))
+        case path => path.replace('\\', '/')
+      }
+    }
+    else platform_path
+  }
+
+
   /* source files */
 
   private def try_file(file: File) = if (file.isFile) Some(file) else None