tuned;

--- a/src/Pure/PIDE/resources.scala	Wed Apr 12 22:32:55 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Apr 12 22:47:21 2017 +0200
@@ -70,7 +70,7 @@
   def theory_qualifier(name: Document.Node.Name): String =
     session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
 
-  def theory_name(qualifier: String, theory0: String): (Boolean, String) =
+  def loaded_theory_name(qualifier: String, theory0: String): (Boolean, String) =
     session_base.loaded_theories.get(theory0) match {
       case Some(theory) => (true, theory)
       case None =>
@@ -82,19 +82,18 @@
     }
 
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
-  {
-    val (loaded, theory) = theory_name(qualifier, Thy_Header.import_name(s))
-    if (loaded) Document.Node.Name.loaded_theory(theory)
-    else
-      session_base.known_theories.get(theory) match {
-        case Some(node_name) => node_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)
-      }
-  }
+    loaded_theory_name(qualifier, Thy_Header.import_name(s)) match {
+      case (true, theory) => Document.Node.Name.loaded_theory(theory)
+      case (false, theory) =>
+        session_base.known_theories.get(theory) match {
+          case Some(node_name) => node_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)
+        }
+    }
 
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {

--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 12 22:32:55 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 12 22:47:21 2017 +0200
@@ -63,9 +63,12 @@
   def node_name(file: JFile): Document.Node.Name =
   {
     val node = file.getPath
-    val (loaded, theory) = theory_name(default_qualifier, Thy_Header.theory_name(node))
-    if (loaded) Document.Node.Name.loaded_theory(theory)
-    else Document.Node.Name(node, if (theory == "") "" else file.getParent, theory)
+    loaded_theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
+      case (true, theory) => Document.Node.Name.loaded_theory(theory)
+      case (false, theory) =>
+        val master_dir = if (theory == "") "" else file.getParent
+        Document.Node.Name(node, master_dir, theory)
+    }
   }
 
   override def append(dir: String, source_path: Path): String =

--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 22:32:55 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 22:47:21 2017 +0200
@@ -29,9 +29,12 @@
   {
     val vfs = VFSManager.getVFSForPath(path)
     val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
-    val (loaded, theory) = theory_name(default_qualifier, Thy_Header.theory_name(node))
-    if (loaded) Document.Node.Name.loaded_theory(theory)
-    else Document.Node.Name(node, if (theory == "") "" else vfs.getParentOfPath(path), theory)
+    loaded_theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
+      case (true, theory) => Document.Node.Name.loaded_theory(theory)
+      case (false, theory) =>
+        val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
+        Document.Node.Name(node, master_dir, theory)
+    }
   }
 
   def node_name(buffer: Buffer): Document.Node.Name =