--- 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)
--- 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)
}