# HG changeset patch
# User wenzelm
# Date 1344939692 -7200
# Node ID 2d6691085b8d9db3b3540b2d7a0b7f3c34b25d34
# Parent  4aa5b965f70ecd24c153905aee190e592bd5c4c5
even more defensive path expansion (see also 8d381fdef898);

diff -r 4aa5b965f70e -r 2d6691085b8d src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 14 11:43:08 2012 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 14 12:21:32 2012 +0200
@@ -51,8 +51,9 @@
     object Name
     {
       val empty = Name("", "", "")
-      def apply(path: Path): Name =
+      def apply(raw_path: Path): Name =
       {
+        val path = raw_path.expand
         val node = path.implode
         val dir = path.dir.implode
         val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)