# HG changeset patch
# User wenzelm
# Date 1492424990 -7200
# Node ID f3076367f4a861b67eff89c2e97f891a718b4ba2
# Parent  331f09d9535ec2701fccc475a41859acf5650fae
tuned signature;

diff -r 331f09d9535e -r f3076367f4a8 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Apr 17 12:20:45 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 17 12:29:50 2017 +0200
@@ -93,6 +93,9 @@
         }
     }
 
+  def import_name(node_name: Document.Node.Name, s: String): Document.Node.Name =
+    import_name(theory_qualifier(node_name), node_name.master_dir, s)
+
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     val path = Path.explode(name.node)
@@ -116,9 +119,7 @@
             " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
-        val imports =
-          header.imports.map({ case (s, pos) =>
-            (import_name(theory_qualifier(node_name), node_name.master_dir, s), pos) })
+        val imports = 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)) }
@@ -135,16 +136,10 @@
 
   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
   {
-    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))
+      if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
+      else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE))
       else Nil
-
     if (imports.isEmpty) None
     else Some(Document.Node.Header(imports.map((_, Position.none))))
   }