src/Pure/Thy/sessions.scala
changeset 65833 95fd3b9888e6
parent 65748 1f4a80e80c88
child 65857 5d29d93766ef
     1.1 --- a/src/Pure/Thy/sessions.scala	Sun May 14 20:16:13 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sun May 14 20:22:54 2017 +0200
     1.3 @@ -37,9 +37,9 @@
     1.4  
     1.5        def local_theories_iterator =
     1.6        {
     1.7 -        val local_path = local_dir.file.getCanonicalFile.toPath
     1.8 +        val local_path = local_dir.canonical_file.toPath
     1.9          theories.iterator.filter(name =>
    1.10 -          Path.explode(name.node).file.getCanonicalFile.toPath.startsWith(local_path))
    1.11 +          Path.explode(name.node).canonical_file.toPath.startsWith(local_path))
    1.12        }
    1.13  
    1.14        val known_theories =
    1.15 @@ -60,7 +60,7 @@
    1.16          (Map.empty[JFile, List[Document.Node.Name]] /:
    1.17              (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
    1.18            case (known, name) =>
    1.19 -            val file = Path.explode(name.node).file.getCanonicalFile
    1.20 +            val file = Path.explode(name.node).canonical_file
    1.21              val theories1 = known.getOrElse(file, Nil)
    1.22              if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
    1.23                known