back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";
--- 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)