# 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)