# HG changeset patch
# User wenzelm
# Date 1492455288 -7200
# Node ID 2af863e28204cab2eb6aa98fb189fc3e7a79bf57
# Parent  7966bd7c64618b04baacbb018fd7891a1fbca675
tuned signature;

diff -r 7966bd7c6461 -r 2af863e28204 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Apr 17 20:33:18 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 17 20:54:48 2017 +0200
@@ -83,7 +83,7 @@
     theory_name(qualifier, Thy_Header.import_name(s)) match {
       case (true, theory) => Document.Node.Name.loaded_theory(theory)
       case (false, theory) =>
-        session_base.known_theories.get(theory) match {
+        session_base.known_theory(theory) match {
           case Some(node_name) => node_name
           case None =>
             val path = Path.explode(s)
diff -r 7966bd7c6461 -r 2af863e28204 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 17 20:33:18 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Apr 17 20:54:48 2017 +0200
@@ -33,7 +33,8 @@
       def bases_iterator(local: Boolean) =
         for {
           base <- bases.iterator
-          (_, name) <- (if (local) base.known_theories_local else base.known_theories).iterator
+          known = base.known
+          (_, name) <- (if (local) known.known_theories_local else known.known_theories).iterator
         } yield name
 
       def local_theories_iterator =
@@ -112,12 +113,14 @@
     def loaded_theory(name: Document.Node.Name): Boolean =
       loaded_theories.isDefinedAt(name.theory)
 
-    def known_theories: Map[String, Document.Node.Name] = known.known_theories
-    def known_theories_local: Map[String, Document.Node.Name] = known.known_theories_local
-    def known_files: Map[JFile, List[Document.Node.Name]] = known.known_files
+    def known_theory(name: String): Option[Document.Node.Name] =
+      known.known_theories.get(name)
+
+    def known_file(file: JFile): Option[Document.Node.Name] =
+      known.known_files.getOrElse(file, Nil).headOption
 
     def dest_known_theories: List[(String, String)] =
-      for ((theory, node_name) <- known_theories.toList)
+      for ((theory, node_name) <- known.known_theories.toList)
         yield (theory, node_name.node)
   }