# HG changeset patch
# User wenzelm
# Date 1491575654 -7200
# Node ID fcff401fb6095544f0ef65f77ea203e0994a7320
# Parent  f8dd71a0791a06be2a60ebd75a1ef168e5ce4374
more explicit lookup of loaded_theories: base names allowed here;
no base names for known_theories;

diff -r f8dd71a0791a -r fcff401fb609 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Apr 07 15:53:06 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Fri Apr 07 16:34:14 2017 +0200
@@ -74,15 +74,14 @@
       if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
       else Long_Name.qualify(session_name, theory0)
 
-    session_base.known_theories.get(theory) orElse session_base.known_theories.get(theory0) match
-    {
-      case Some(name) =>
-        if (session_base.loaded_theory(name)) name.loaded_theory else name
-      case None =>
-        val path = Path.explode(s)
-        val node = append(dir, thy_path(path))
-        val master_dir = append(dir, path.dir)
-        Document.Node.Name(node, master_dir, theory)
+    session_base.loaded_theories.get(theory) orElse
+    session_base.loaded_theories.get(theory0) orElse
+    session_base.known_theories.get(theory) orElse
+    session_base.known_theories.get(theory0) getOrElse {
+      val path = Path.explode(s)
+      val node = append(dir, thy_path(path))
+      val master_dir = append(dir, path.dir)
+      Document.Node.Name(node, master_dir, theory)
     }
   }
 
diff -r f8dd71a0791a -r fcff401fb609 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Apr 07 15:53:06 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 16:34:14 2017 +0200
@@ -40,9 +40,7 @@
           known.get(name.theory) match {
             case Some(name1) if name != name1 =>
               error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
-            case _ =>
-              known + (name.theory -> name) +
-                (Long_Name.base_name(name.theory) -> name)  // legacy
+            case _ => known + (name.theory -> name)
           }
         })
     }
@@ -50,7 +48,7 @@
 
   sealed case class Base(
     global_theories: Set[String] = Set.empty,
-    loaded_theories: Set[String] = Set.empty,
+    loaded_theories: Map[String, Document.Node.Name] = Map.empty,
     known_theories: Map[String, Document.Node.Name] = Map.empty,
     keywords: Thy_Header.Keywords = Nil,
     syntax: Outer_Syntax = Outer_Syntax.empty,
@@ -58,7 +56,7 @@
     session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
   {
     def loaded_theory(name: Document.Node.Name): Boolean =
-      loaded_theories.contains(name.theory)
+      loaded_theories.isDefinedAt(name.theory)
   }
 
   sealed case class Deps(sessions: Map[String, Base])
diff -r f8dd71a0791a -r fcff401fb609 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri Apr 07 15:53:06 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Fri Apr 07 16:34:14 2017 +0200
@@ -67,7 +67,7 @@
       val import_errors =
         (for {
           (theory, imports) <- seen_theory.iterator_list
-          if !resources.session_base.loaded_theories(theory)
+          if !resources.session_base.loaded_theories.isDefinedAt(theory)
           if imports.length > 1
         } yield {
           "Incoherent imports for theory " + quote(theory) + ":\n" +
@@ -80,11 +80,12 @@
     lazy val syntax: Outer_Syntax =
       resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
 
-    def loaded_theories: Set[String] =
+    def loaded_theories: Map[String, Document.Node.Name] =
       (resources.session_base.loaded_theories /: rev_deps) {
         case (loaded, dep) =>
-          loaded + dep.name.theory +
-            Long_Name.base_name(dep.name.theory)  // legacy
+          val name = dep.name.loaded_theory
+          loaded + (name.theory -> name) +
+            (Long_Name.base_name(name.theory) -> name)  // legacy
       }
 
     def loaded_files: List[Path] =