back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";
authorwenzelm
Tue, 04 Apr 2017 16:18:53 +0200
changeset 65368 7fb5aad28f38
parent 65367 83c30e290702
child 65369 27c1b5e952bd
back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";
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)