# HG changeset patch
# User wenzelm
# Date 1491222584 -7200
# Node ID e345e94201093b00fcb3a7f0dae4489508a68f2b
# Parent  9a2c266f97c805ae34044a72e14476718433abe1
proper qualifier (again, see df4cd6e1fdfa);

diff -r 9a2c266f97c8 -r e345e9420109 src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Mon Apr 03 13:39:13 2017 +0200
+++ b/src/Pure/General/long_name.ML	Mon Apr 03 14:29:44 2017 +0200
@@ -64,4 +64,3 @@
       in implode (nth_map (length names - 1) f names) end;
 
 end;
-
diff -r 9a2c266f97c8 -r e345e9420109 src/Pure/General/long_name.scala
--- a/src/Pure/General/long_name.scala	Mon Apr 03 13:39:13 2017 +0200
+++ b/src/Pure/General/long_name.scala	Mon Apr 03 14:29:44 2017 +0200
@@ -25,4 +25,3 @@
     if (name == "") ""
     else explode(name).last
 }
-
diff -r 9a2c266f97c8 -r e345e9420109 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Apr 03 13:39:13 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 14:29:44 2017 +0200
@@ -24,10 +24,9 @@
 
   def node_name(qualifier: String, raw_path: Path): Document.Node.Name =
   {
-    val no_qualifier = "" // FIXME
     val path = raw_path.expand
     val node = path.implode
-    val theory = Long_Name.qualify(no_qualifier, Thy_Header.thy_name(node).getOrElse(""))
+    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)
   }
@@ -79,9 +78,8 @@
 
   def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
   {
-    val no_qualifier = "" // FIXME
     val thy1 = Thy_Header.base_name(s)
-    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1)
+    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(qualifier, thy1)
     (base.known_theories.get(thy1) orElse
      base.known_theories.get(thy2) orElse
      base.known_theories.get(Long_Name.base_name(thy1))) match {
@@ -94,7 +92,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(no_qualifier, theory))
+          Document.Node.Name(node, master_dir, Long_Name.qualify(qualifier, theory))
         }
     }
   }