# HG changeset patch
# User wenzelm
# Date 1245941323 -7200
# Node ID 5fb98777c3a6d60a05cf104c02a42e56c20da382
# Parent  2f0adf64985b86842b6d028a9ebe49a3852677e4# Parent  4aabae982988d008128d5894f6b4973cfa96a227
merged

diff -r 2f0adf64985b -r 5fb98777c3a6 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Jun 25 15:42:36 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Jun 25 16:48:43 2009 +0200
@@ -144,11 +144,25 @@
     def append(path: String)
     {
       init(path)
-      for (p <- path.split("/") if p != "") {
-        val len = result_path.length
-        if (len > 0 && result_path(len - 1) != '/')
-          result_path += '/'
-        result_path ++= p
+      for (p <- path.split("/") if p != "" && p != ".") {
+        if (p == "..") {
+          val result = result_path.toString
+          val i = result.lastIndexOf("/")
+          if (result == "")
+            result_path ++= ".."
+          else if (result.substring(i + 1) == "..")
+            result_path ++= "/.."
+          else if (i < 1)
+            result_path.length = i + 1
+          else
+            result_path.length = i
+        }
+        else {
+          val len = result_path.length
+          if (len > 0 && result_path(len - 1) != '/')
+            result_path += '/'
+          result_path ++= p
+        }
       }
     }
     init(source_path)