# HG changeset patch
# User haftmann
# Date 1245942448 -7200
# Node ID 235b12db0cf38eac4330dce05405faa8bbf721f3
# Parent  5fb98777c3a6d60a05cf104c02a42e56c20da382# Parent  039893a9a77d11b46d18b66fe8f768090bc6403e
merged

diff -r 039893a9a77d -r 235b12db0cf3 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Jun 25 17:07:18 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Jun 25 17:07:28 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)