src/Pure/PIDE/resources.scala
changeset 65472 f83081bcdd0e
parent 65471 05e5bffcf1d8
child 65476 a72ae9eb4462
--- 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 =
   {