# HG changeset patch
# User wenzelm
# Date 1245940448 -7200
# Node ID 4aabae982988d008128d5894f6b4973cfa96a227
# Parent  a36b5e02c1abbd1fc8d1d30cb3f073f10c6c3ab9
expand_path: handle parent (..) elements;

diff -r a36b5e02c1ab -r 4aabae982988 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Jun 25 13:40:03 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Jun 25 16:34:08 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)