# HG changeset patch
# User wenzelm
# Date 1491315533 -7200
# Node ID 7fb5aad28f384d620088b67fba8f0d22589922fd
# Parent  83c30e29070217c516f7a412b7b394bcb0540ac6
back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";

diff -r 83c30e290702 -r 7fb5aad28f38 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Apr 04 15:05:00 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Apr 04 16:18:53 2017 +0200
@@ -80,15 +80,12 @@
   def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
   {
     val theory = Thy_Header.base_name(s)
-    val is_base_name = Thy_Header.is_base_name(s)
-    val is_qualified = is_base_name && Long_Name.is_qualified(s)
+    val is_qualified = Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)
 
     val known_theory =
-      if (is_base_name)
-        session_base.known_theories.get(theory) orElse
-        (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
-         else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
-      else None
+      session_base.known_theories.get(theory) orElse
+      (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
+       else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
 
     known_theory match {
       case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)