# HG changeset patch
# User wenzelm
# Date 1491487053 -7200
# Node ID c728f922f6578bc4718f0c8f6793d2207b330adb
# Parent  4546272431e90315e2e68ace92125bbe6984d160
more accurate qualified lookup;
tuned;

diff -r 4546272431e9 -r c728f922f657 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Apr 06 15:44:16 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Apr 06 15:57:33 2017 +0200
@@ -69,24 +69,19 @@
 
   def import_name(dir: String, s: String): Document.Node.Name =
   {
-    val thy = Thy_Header.base_name(s)
-    val is_global = session_base.global_theories.contains(thy)
-    val is_qualified = Long_Name.is_qualified(thy)
+    val theory0 = Thy_Header.base_name(s)
+    val theory =
+      if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
+      else Long_Name.qualify(session_name, theory0)
 
-    val known_theory =
-      session_base.known_theories.get(thy) orElse
-      (if (is_global) None
-       else if (is_qualified) session_base.known_theories.get(Long_Name.base_name(thy))
-       else session_base.known_theories.get(Long_Name.qualify(session_name, thy)))
-
-    known_theory match {
+    session_base.known_theories.get(theory) orElse session_base.known_theories.get(theory0) match
+    {
       case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
       case Some(name) => name
       case None =>
         val path = Path.explode(s)
         val node = append(dir, thy_path(path))
         val master_dir = append(dir, path.dir)
-        val theory = if (is_global || is_qualified) thy else Long_Name.qualify(session_name, thy)
         Document.Node.Name(node, master_dir, theory)
     }
   }