# HG changeset patch
# User wenzelm
# Date 1511903650 -3600
# Node ID a2fa0c6a7aff4cd791e47393def302e345d4c18a
# Parent  39cc38a06610513036db39e9e26f70cf29fe83d9
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);

diff -r 39cc38a06610 -r a2fa0c6a7aff src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Nov 27 16:57:34 2017 +0100
+++ b/src/Pure/PIDE/resources.ML	Tue Nov 28 22:14:10 2017 +0100
@@ -108,26 +108,24 @@
   | NONE => Long_Name.qualifier theory);
 
 fun theory_name qualifier theory =
-  if loaded_theory theory then (true, theory)
-  else
-    let val theory' =
-      if Long_Name.is_qualified theory orelse is_some (global_theory theory)
-      then theory
-      else Long_Name.qualify qualifier theory
-    in (false, theory') end;
+  if Long_Name.is_qualified theory orelse is_some (global_theory theory)
+  then theory
+  else Long_Name.qualify qualifier theory;
 
 fun import_name qualifier dir s =
-  (case theory_name qualifier (Thy_Header.import_name s) of
-    (true, theory) => {master_dir = Path.current, theory_name = theory}
-  | (false, theory) =>
-      let val node_name =
-        (case known_theory theory of
-          SOME node_name => node_name
-        | NONE =>
-            if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
-            then Path.explode s
-            else File.full_path dir (thy_path (Path.expand (Path.explode s))))
-      in {master_dir = Path.dir node_name, theory_name = theory} end);
+  let val theory = theory_name qualifier (Thy_Header.import_name s) in
+    if loaded_theory theory then {master_dir = Path.current, theory_name = theory}
+    else
+      let
+        val node_name =
+          (case known_theory theory of
+            SOME node_name => node_name
+          | NONE =>
+              if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
+              then Path.explode s
+              else File.full_path dir (thy_path (Path.expand (Path.explode s))));
+      in {master_dir = Path.dir node_name, theory_name = theory} end
+  end;
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
diff -r 39cc38a06610 -r a2fa0c6a7aff src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Nov 27 16:57:34 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Nov 28 22:14:10 2017 +0100
@@ -86,33 +86,30 @@
     roots ::: files
   }
 
-  def theory_name(qualifier: String, theory: String): (Boolean, String) =
-    if (session_base.loaded_theory(theory)) (true, theory)
-    else {
-      val theory1 =
-        if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
-          theory
-        else Long_Name.qualify(qualifier, theory)
-      (false, theory1)
-    }
+  def theory_name(qualifier: String, theory: String): String =
+    if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
+      theory
+    else Long_Name.qualify(qualifier, theory)
 
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
-    theory_name(qualifier, Thy_Header.import_name(s)) match {
-      case (true, theory) => Document.Node.Name.loaded_theory(theory)
-      case (false, theory) =>
-        session_base.known_theory(theory) match {
-          case Some(node_name) => node_name
-          case None =>
-            if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s))
-              Document.Node.Name.loaded_theory(theory)
-            else {
-              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)
-            }
-        }
+  {
+    val theory = theory_name(qualifier, Thy_Header.import_name(s))
+    if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+    else {
+      session_base.known_theory(theory) match {
+        case Some(node_name) => node_name
+        case None =>
+          if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s))
+            Document.Node.Name.loaded_theory(theory)
+          else {
+            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 import_name(name: Document.Node.Name, s: String): Document.Node.Name =
     import_name(session_base.theory_qualifier(name), name.master_dir, s)
diff -r 39cc38a06610 -r a2fa0c6a7aff src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Nov 27 16:57:34 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Nov 28 22:14:10 2017 +0100
@@ -93,11 +93,11 @@
   def node_name(file: JFile): Document.Node.Name =
     session_base.known.get_file(file, bootstrap = true) getOrElse {
       val node = file.getPath
-      theory_name(Sessions.DRAFT, 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)
+      val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
+      if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+      else {
+        val master_dir = if (theory == "") "" else file.getParent
+        Document.Node.Name(node, master_dir, theory)
       }
     }
 
diff -r 39cc38a06610 -r a2fa0c6a7aff src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Nov 27 16:57:34 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Nov 28 22:14:10 2017 +0100
@@ -43,11 +43,11 @@
     known_file(path) getOrElse {
       val vfs = VFSManager.getVFSForPath(path)
       val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
-      theory_name(Sessions.DRAFT, 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)
+      val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
+      if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+      else {
+        val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
+        Document.Node.Name(node, master_dir, theory)
       }
     }