diff -r e345e9420109 -r 9ca34f0407a9 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Apr 03 14:29:44 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 16:36:45 2017 +0200
@@ -13,25 +13,16 @@
 import java.io.{File => JFile}
 
 
-class Resources(val base: Sessions.Base, val log: Logger = No_Logger)
+class Resources(
+  val session_name: String,
+  val base: Sessions.Base,
+  val log: Logger = No_Logger)
 {
   val thy_info = new Thy_Info(this)
 
   def thy_path(path: Path): Path = path.ext("thy")
 
 
-  /* document node names */
-
-  def node_name(qualifier: String, raw_path: Path): Document.Node.Name =
-  {
-    val path = raw_path.expand
-    val node = path.implode
-    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
-    val master_dir = if (theory == "") "" else path.dir.implode
-    Document.Node.Name(node, master_dir, theory)
-  }
-
-
   /* file-system operations */
 
   def append(dir: String, source_path: Path): String =
@@ -76,10 +67,20 @@
     }
     else Nil
 
-  def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
+  def init_name(global: Boolean, raw_path: Path): Document.Node.Name =
+  {
+    val path = raw_path.expand
+    val node = path.implode
+    val qualifier = if (global) "" else session_name
+    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
+    val master_dir = if (theory == "") "" else path.dir.implode
+    Document.Node.Name(node, master_dir, theory)
+  }
+
+  def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
   {
     val thy1 = Thy_Header.base_name(s)
-    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(qualifier, thy1)
+    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(session_name, thy1)
     (base.known_theories.get(thy1) orElse
      base.known_theories.get(thy2) orElse
      base.known_theories.get(Long_Name.base_name(thy1))) match {
@@ -92,7 +93,7 @@
         else {
           val node = append(master.master_dir, thy_path(path))
           val master_dir = append(master.master_dir, path.dir)
-          Document.Node.Name(node, master_dir, Long_Name.qualify(qualifier, theory))
+          Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory))
         }
     }
   }
@@ -106,9 +107,8 @@
     try { f(reader) } finally { reader.close }
   }
 
-  def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
-      reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true)
-    : Document.Node.Header =
+  def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char],
+    start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
   {
     if (node_name.is_theory && reader.source.length > 0) {
       try {
@@ -122,7 +122,7 @@
             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
         val imports =
-          header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
+          header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
         Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
@@ -130,18 +130,18 @@
     else Document.Node.no_header
   }
 
-  def check_thy(qualifier: String, name: Document.Node.Name,
-      start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
-    with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict))
+  def check_thy(name: Document.Node.Name, start: Token.Pos = Token.Pos.command,
+      strict: Boolean = true): Document.Node.Header =
+    with_thy_reader(name, check_thy_reader(name, _, start, strict))
 
 
   /* special header */
 
   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
     if (Thy_Header.is_ml_root(name.theory))
-      Some(Document.Node.Header(List((import_name("", name, Thy_Header.ML_BOOTSTRAP), Position.none))))
+      Some(Document.Node.Header(List((import_name(name, Thy_Header.ML_BOOTSTRAP), Position.none))))
     else if (Thy_Header.is_bootstrap(name.theory))
-      Some(Document.Node.Header(List((import_name("", name, Thy_Header.PURE), Position.none))))
+      Some(Document.Node.Header(List((import_name(name, Thy_Header.PURE), Position.none))))
     else None