clarified loaded_theories: map to qualified theory name;
proper theory_name for PIDE editors;

--- a/src/Pure/PIDE/document.scala	Wed Apr 12 21:13:43 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Apr 12 22:32:55 2017 +0200
@@ -99,6 +99,8 @@
     {
       val empty = Name("")
 
+      def loaded_theory(theory: String): Name = Name(theory, "", theory)
+
       object Ordering extends scala.math.Ordering[Name]
       {
         def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
@@ -114,7 +116,6 @@
           case _ => false
         }
 
-      def loaded_theory: Name = Name(theory, "", theory)
       def is_theory: Boolean = theory.nonEmpty
 
       def theory_base_name: String = Long_Name.base_name(theory)

--- a/src/Pure/PIDE/protocol.scala	Wed Apr 12 21:13:43 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Apr 12 22:32:55 2017 +0200
@@ -314,7 +314,7 @@
     protocol_command("Prover.session_base",
       Symbol.encode(resources.default_qualifier),
       encode_table(resources.session_base.global_theories.toList),
-      encode_table(resources.session_base.dest_loaded_theories),
+      encode_table(resources.session_base.loaded_theories.toList),
       encode_table(resources.session_base.dest_known_theories))
 
 

--- a/src/Pure/PIDE/resources.ML	Wed Apr 12 21:13:43 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Wed Apr 12 22:32:55 2017 +0200
@@ -14,7 +14,7 @@
   val reset_session_base: unit -> unit
   val default_qualifier: unit -> string
   val global_theory: string -> string option
-  val loaded_theory: string -> Path.T option
+  val loaded_theory: string -> string option
   val known_theory: string -> Path.T option
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
@@ -43,7 +43,7 @@
 val init_session_base =
   {default_qualifier = "Draft",
    global_theories = Symtab.empty: string Symtab.table,
-   loaded_theories = Symtab.empty: Path.T Symtab.table,
+   loaded_theories = Symtab.empty: string Symtab.table,
    known_theories = Symtab.empty: Path.T Symtab.table};
 
 val global_session_base =
@@ -56,7 +56,7 @@
         if default_qualifier <> "" then default_qualifier
         else #default_qualifier init_session_base,
        global_theories = Symtab.make global_theories,
-       loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
+       loaded_theories = Symtab.make loaded_theories,
        known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
 
 fun reset_session_base () =
@@ -108,20 +108,24 @@
     SOME qualifier => qualifier
   | NONE => Long_Name.qualifier theory);
 
+fun theory_name qualifier theory0 =
+  (case loaded_theory theory0 of
+    SOME theory => (true, theory)
+  | NONE =>
+      (false,
+        if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
+          orelse true (* FIXME *) then theory0
+        else Long_Name.qualify qualifier theory0));
+
 fun import_name qualifier dir s =
   let
-    val theory0 = Thy_Header.import_name s;
-    val theory =
-      if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
-        orelse true (* FIXME *) then theory0
-      else Long_Name.qualify qualifier theory0;
+    val (loaded, theory) = theory_name qualifier (Thy_Header.import_name s);
     val node_name =
-      the (get_first (fn e => e ())
-        [fn () => loaded_theory theory,
-         fn () => loaded_theory theory0,
-         fn () => known_theory theory,
-         fn () => known_theory theory0,
-         fn () => SOME (File.full_path dir (thy_path (Path.expand (Path.explode s))))])
+      if loaded then Path.basic theory
+      else
+        (case known_theory theory of
+          SOME node_name => node_name
+        | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))));
   in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end;
 
 fun check_file dir file = File.check_file (File.full_path dir file);

--- a/src/Pure/PIDE/resources.scala	Wed Apr 12 21:13:43 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Apr 12 22:32:55 2017 +0200
@@ -70,23 +70,30 @@
   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) =
+    session_base.loaded_theories.get(theory0) match {
+      case Some(theory) => (true, theory)
+      case None =>
+        val theory =
+          if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0)
+              || true /* FIXME */) theory0
+          else Long_Name.qualify(qualifier, theory0)
+        (false, theory)
+    }
+
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
   {
-    val theory0 = Thy_Header.import_name(s)
-    val theory =
-      if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0)
-        || true /* FIXME */) theory0
-      else Long_Name.qualify(qualifier, theory0)
-
-    session_base.loaded_theories.get(theory) orElse
-    session_base.loaded_theories.get(theory0) orElse
-    session_base.known_theories.get(theory) orElse
-    session_base.known_theories.get(theory0) getOrElse {
-      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 (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)
+      }
   }
 
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =

--- a/src/Pure/Thy/sessions.scala	Wed Apr 12 21:13:43 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Apr 12 22:32:55 2017 +0200
@@ -85,7 +85,7 @@
 
   sealed case class Base(
     global_theories: Map[String, String] = Map.empty,
-    loaded_theories: Map[String, Document.Node.Name] = Map.empty,
+    loaded_theories: Map[String, String] = Map.empty,
     known_theories: Map[String, Document.Node.Name] = Map.empty,
     known_theories_local: Map[String, Document.Node.Name] = Map.empty,
     known_files: Map[JFile, List[Document.Node.Name]] = Map.empty,
@@ -96,8 +96,6 @@
   {
     def platform_path: Base =
       copy(
-        loaded_theories =
-          for ((a, b) <- loaded_theories) yield (a, b.map(File.platform_path(_))),
         known_theories =
           for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))),
         known_theories_local =
@@ -108,10 +106,6 @@
     def loaded_theory(name: Document.Node.Name): Boolean =
       loaded_theories.isDefinedAt(name.theory)
 
-    def dest_loaded_theories: List[(String, String)] =
-      for ((theory, node_name) <- loaded_theories.toList)
-        yield (theory, node_name.node)
-
     def dest_known_theories: List[(String, String)] =
       for ((theory, node_name) <- known_theories.toList)
         yield (theory, node_name.node)

--- a/src/Pure/Thy/thy_info.scala	Wed Apr 12 21:13:43 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Wed Apr 12 22:32:55 2017 +0200
@@ -80,12 +80,12 @@
     lazy val syntax: Outer_Syntax =
       resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
 
-    def loaded_theories: Map[String, Document.Node.Name] =
+    def loaded_theories: Map[String, String] =
       (resources.session_base.loaded_theories /: rev_deps) {
         case (loaded, dep) =>
-          val name = dep.name.loaded_theory
-          loaded + (name.theory -> name) +
-            (name.theory_base_name -> name)  // legacy
+          val name = dep.name
+          loaded + (name.theory -> name.theory) +
+            (name.theory_base_name -> name.theory)  // legacy
       }
 
     def loaded_files: List[Path] =

--- a/src/Pure/Tools/build.scala	Wed Apr 12 21:13:43 2017 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 12 22:32:55 2017 +0200
@@ -205,14 +205,14 @@
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
                 pair(list(pair(Options.encode, list(string))),
-                pair(list(pair(string, string)),
-                pair(list(pair(string, string)), list(pair(string, string))))))))))))))))(
+                pair(list(pair(string, string)), pair(list(pair(string, string)),
+                list(pair(string, string))))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
                 (parent, (info.chapter, (name, (Path.current,
                 (info.theories,
-                (base.global_theories.toList,
-                (base.dest_loaded_theories, base.dest_known_theories)))))))))))))))
+                (base.global_theories.toList, (base.loaded_theories.toList,
+                base.dest_known_theories)))))))))))))))
             })
 
         val env =

--- a/src/Pure/Tools/ml_process.scala	Wed Apr 12 21:13:43 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala	Wed Apr 12 22:32:55 2017 +0200
@@ -101,7 +101,7 @@
                 ML_Syntax.print_string, ML_Syntax.print_string))(table)
           List("Resources.set_session_base {default_qualifier = \"\"" +
             ", global_theories = " + print_table(base.global_theories.toList) +
-            ", loaded_theories = " + print_table(base.dest_loaded_theories) +
+            ", loaded_theories = " + print_table(base.loaded_theories.toList) +
             ", known_theories = " + print_table(base.dest_known_theories) + "}")
       }
 

--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 12 21:13:43 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 12 22:32:55 2017 +0200
@@ -63,9 +63,9 @@
   def node_name(file: JFile): Document.Node.Name =
   {
     val node = file.getPath
-    val theory = Thy_Header.theory_name(node)
-    val master_dir = if (theory == "") "" else file.getParent
-    Document.Node.Name(node, master_dir, theory)
+    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)
   }
 
   override def append(dir: String, source_path: Path): String =

--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 21:13:43 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 22:32:55 2017 +0200
@@ -29,9 +29,9 @@
   {
     val vfs = VFSManager.getVFSForPath(path)
     val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
-    val theory = Thy_Header.theory_name(node)
-    val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
-    Document.Node.Name(node, master_dir, theory)
+    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)
   }
 
   def node_name(buffer: Buffer): Document.Node.Name =