uniform import_name, with treatment of global and qualified theories;

--- a/src/Pure/PIDE/resources.scala	Wed Apr 05 11:39:36 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Apr 05 22:00:44 2017 +0200
@@ -67,38 +67,27 @@
     }
     else Nil
 
-  def qualify(name: String): String =
-    if (session_base.global_theories.contains(name) || Long_Name.is_qualified(name)) name
-    else Long_Name.qualify(session_name, name)
-
-  def init_name(raw_path: Path): Document.Node.Name =
+  def import_name(dir: String, s: String): Document.Node.Name =
   {
-    val path = raw_path.expand
-    val node = path.implode
-    val theory = qualify(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 theory = Thy_Header.base_name(s)
-    val is_qualified = Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)
+    val thy = Thy_Header.base_name(s)
+    val is_global = session_base.global_theories.contains(thy)
+    val is_qualified = Long_Name.is_qualified(thy)
 
     val known_theory =
-      session_base.known_theories.get(theory) orElse
-      (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
-       else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
+      session_base.known_theories.get(thy) orElse
+      (if (is_global) None
+       else if (is_qualified) session_base.known_theories.get(Long_Name.base_name(thy))
+       else session_base.known_theories.get(Long_Name.qualify(session_name, thy)))
 
     known_theory match {
       case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
       case Some(name) => name
-      case None if is_qualified => Document.Node.Name.theory(theory)
       case None =>
         val path = Path.explode(s)
-        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(session_name, theory))
+        val node = append(dir, thy_path(path))
+        val master_dir = append(dir, path.dir)
+        val theory = if (is_global || is_qualified) thy else Long_Name.qualify(session_name, thy)
+        Document.Node.Name(node, master_dir, theory)
     }
   }
 
@@ -126,7 +115,7 @@
             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
         val imports =
-          header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
+          header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) })
         Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
@@ -143,9 +132,11 @@
 
   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.master_dir, 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.master_dir, Thy_Header.PURE), Position.none))))
     else None
 
 

--- a/src/Pure/Thy/sessions.scala	Wed Apr 05 11:39:36 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Apr 05 22:00:44 2017 +0200
@@ -81,8 +81,7 @@
             {
               val root_theories =
                 info.theories.flatMap({ case (_, thys) =>
-                  thys.map(thy =>
-                    (resources.init_name(info.dir + resources.thy_path(thy)), info.pos))
+                  thys.map(thy => (resources.import_name(info.dir.implode, thy), info.pos))
                 })
               val thy_deps = resources.thy_info.dependencies(root_theories)
 
@@ -174,7 +173,7 @@
     parent: Option[String],
     description: String,
     options: Options,
-    theories: List[(Options, List[Path])],
+    theories: List[(Options, List[String])],
     global_theories: List[String],
     files: List[Path],
     document_files: List[(Path, Path)],
@@ -389,8 +388,7 @@
           val session_options = options ++ entry.options
 
           val theories =
-            entry.theories.map({ case (opts, thys) =>
-              (session_options ++ opts, thys.map(thy => Path.explode(thy._1))) })
+            entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
 
           val global_theories =
             for { (_, thys) <- entry.theories; (thy, global) <- thys if global }

--- a/src/Pure/Thy/thy_header.scala	Wed Apr 05 11:39:36 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala	Wed Apr 05 22:00:44 2017 +0200
@@ -80,9 +80,6 @@
   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
 
-  def is_base_name(s: String): Boolean =
-    s != "" && !s.exists("/\\:".contains(_))
-
   def base_name(s: String): String =
     s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
 

--- a/src/Pure/Tools/build.scala	Wed Apr 05 11:39:36 2017 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 05 22:00:44 2017 +0200
@@ -204,7 +204,7 @@
               pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
-                list(pair(Options.encode, list(Path.encode))))))))))))))(
+                list(pair(Options.encode, list(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,