even more defensive path expansion (see also 8d381fdef898);
authorwenzelm
Tue Aug 14 12:21:32 2012 +0200 (2012-08-14 ago)
changeset 487932d6691085b8d
parent 48792 4aa5b965f70e
child 48794 8d2a026e576b
even more defensive path expansion (see also 8d381fdef898);
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 14 11:43:08 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 14 12:21:32 2012 +0200
     1.3 @@ -51,8 +51,9 @@
     1.4      object Name
     1.5      {
     1.6        val empty = Name("", "", "")
     1.7 -      def apply(path: Path): Name =
     1.8 +      def apply(raw_path: Path): Name =
     1.9        {
    1.10 +        val path = raw_path.expand
    1.11          val node = path.implode
    1.12          val dir = path.dir.implode
    1.13          val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)