src/Pure/Thy/sessions.scala

   {
     def platform_path: Known =
       copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
         theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
         files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
+
+    def get_file(file: JFile): Option[Document.Node.Name] =
+      files.getOrElse(file.getCanonicalFile, Nil).headOption
   }
 
   object Base
   {
     def pure(options: Options): Base = session_base(options, Thy_Header.PURE)

     def loaded_theory(name: Document.Node.Name): Boolean =
       loaded_theories.isDefinedAt(name.theory)
 
     def known_theory(name: String): Option[Document.Node.Name] =
       known.theories.get(name)
-
-    def known_file(file: JFile): Option[Document.Node.Name] =
-      known.files.getOrElse(file.getCanonicalFile, Nil).headOption
 
     def dest_known_theories: List[(String, String)] =
       for ((theory, node_name) <- known.theories.toList)
         yield (theory, node_name.node)
   }