clarified: Map index uses canonical files;
authorwenzelm
Mon Apr 17 21:26:23 2017 +0200 (2017-04-17)
changeset 65500a6644e0e8728
parent 65499 fc7f03cbccbc
child 65501 b42743f5b595
clarified: Map index uses canonical files;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Apr 17 21:00:38 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Apr 17 21:26:23 2017 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4        known.theories.get(name)
     1.5  
     1.6      def known_file(file: JFile): Option[Document.Node.Name] =
     1.7 -      known.files.getOrElse(file, Nil).headOption
     1.8 +      known.files.getOrElse(file.getCanonicalFile, Nil).headOption
     1.9  
    1.10      def dest_known_theories: List[(String, String)] =
    1.11        for ((theory, node_name) <- known.theories.toList)