# HG changeset patch
# User wenzelm
# Date 1399558756 -7200
# Node ID df4cd6e1fdfae11bb63b9b60247ad0131cb71b5f
# Parent  293cd4dcfebca7fc36b48555bb1c09b12eb7731e
no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;

diff -r 293cd4dcfebc -r df4cd6e1fdfa src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu May 08 16:15:20 2014 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu May 08 16:19:16 2014 +0200
@@ -28,9 +28,10 @@
 
   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(qualifier, Thy_Header.thy_name(node).getOrElse(""))
+    val theory = Long_Name.qualify(no_qualifier, Thy_Header.thy_name(node).getOrElse(""))
     val master_dir = if (theory == "") "" else path.dir.implode
     Document.Node.Name(node, master_dir, theory)
   }
@@ -65,8 +66,9 @@
 
   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(qualifier, thy1)
+    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1)
     (known_theories.get(thy1) orElse
      known_theories.get(thy2) orElse
      known_theories.get(Long_Name.base_name(thy1))) match {
@@ -79,7 +81,7 @@
         else {
           val node = append(master.master_dir, Resources.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(no_qualifier, theory))
         }
     }
   }