src/Pure/Thy/sessions.scala
changeset 65524 0910f1733909
parent 65520 f47bc12b6e8a
child 65525 360063716c71
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Apr 20 14:59:57 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Apr 20 15:00:32 2017 +0200
     1.3 @@ -81,6 +81,9 @@
     1.4        copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
     1.5          theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
     1.6          files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
     1.7 +
     1.8 +    def get_file(file: JFile): Option[Document.Node.Name] =
     1.9 +      files.getOrElse(file.getCanonicalFile, Nil).headOption
    1.10    }
    1.11  
    1.12    object Base
    1.13 @@ -111,9 +114,6 @@
    1.14      def known_theory(name: String): Option[Document.Node.Name] =
    1.15        known.theories.get(name)
    1.16  
    1.17 -    def known_file(file: JFile): Option[Document.Node.Name] =
    1.18 -      known.files.getOrElse(file.getCanonicalFile, Nil).headOption
    1.19 -
    1.20      def dest_known_theories: List[(String, String)] =
    1.21        for ((theory, node_name) <- known.theories.toList)
    1.22          yield (theory, node_name.node)