src/Pure/PIDE/resources.scala
changeset 65445 e9e7f5f5794c
parent 65441 9425e4d8bdb6
child 65452 9e9750a7932c
--- a/src/Pure/PIDE/resources.scala	Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Sat Apr 08 22:36:32 2017 +0200
@@ -15,7 +15,7 @@
 
 class Resources(
   val session_base: Sessions.Base,
-  val default_qualifier: String = "",
+  val default_qualifier: String = Sessions.DRAFT,
   val log: Logger = No_Logger)
 {
   val thy_info = new Thy_Info(this)
@@ -67,12 +67,16 @@
     }
     else Nil
 
-  def import_name(dir: String, s: String): Document.Node.Name =
+  def theory_qualifier(name: Document.Node.Name): String =
+    Long_Name.qualifier(name.theory)
+
+  def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
   {
     val theory0 = Thy_Header.base_name(s)
     val theory =
-      if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
-      else Long_Name.qualify(default_qualifier, theory0)
+      if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)
+        || true /* FIXME */) theory0
+      else theory0 // FIXME Long_Name.qualify(qualifier, theory0)
 
     session_base.loaded_theories.get(theory) orElse
     session_base.loaded_theories.get(theory0) orElse
@@ -109,7 +113,8 @@
             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
         val imports =
-          header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) })
+          header.imports.map({ case (s, pos) =>
+            (import_name(theory_qualifier(node_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)) }
@@ -125,13 +130,20 @@
   /* 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.master_dir, Thy_Header.ML_BOOTSTRAP), Position.none))))
-    else if (Thy_Header.is_bootstrap(name.theory))
-      Some(Document.Node.Header(
-        List((import_name(name.master_dir, Thy_Header.PURE), Position.none))))
-    else None
+  {
+    val qualifier = theory_qualifier(name)
+    val dir = name.master_dir
+
+    val imports =
+      if (Thy_Header.is_ml_root(name.theory))
+        List(import_name(qualifier, dir, Thy_Header.ML_BOOTSTRAP))
+      else if (Thy_Header.is_bootstrap(name.theory))
+        List(import_name(qualifier, dir, Thy_Header.PURE))
+      else Nil
+
+    if (imports.isEmpty) None
+    else Some(Document.Node.Header(imports.map((_, Position.none))))
+  }
 
 
   /* blobs */