src/Pure/PIDE/resources.scala
changeset 65358 e345e9420109
parent 65357 9a2c266f97c8
child 65359 9ca34f0407a9
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 03 13:39:13 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 14:29:44 2017 +0200
     1.3 @@ -24,10 +24,9 @@
     1.4  
     1.5    def node_name(qualifier: String, raw_path: Path): Document.Node.Name =
     1.6    {
     1.7 -    val no_qualifier = "" // FIXME
     1.8      val path = raw_path.expand
     1.9      val node = path.implode
    1.10 -    val theory = Long_Name.qualify(no_qualifier, Thy_Header.thy_name(node).getOrElse(""))
    1.11 +    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
    1.12      val master_dir = if (theory == "") "" else path.dir.implode
    1.13      Document.Node.Name(node, master_dir, theory)
    1.14    }
    1.15 @@ -79,9 +78,8 @@
    1.16  
    1.17    def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
    1.18    {
    1.19 -    val no_qualifier = "" // FIXME
    1.20      val thy1 = Thy_Header.base_name(s)
    1.21 -    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1)
    1.22 +    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(qualifier, thy1)
    1.23      (base.known_theories.get(thy1) orElse
    1.24       base.known_theories.get(thy2) orElse
    1.25       base.known_theories.get(Long_Name.base_name(thy1))) match {
    1.26 @@ -94,7 +92,7 @@
    1.27          else {
    1.28            val node = append(master.master_dir, thy_path(path))
    1.29            val master_dir = append(master.master_dir, path.dir)
    1.30 -          Document.Node.Name(node, master_dir, Long_Name.qualify(no_qualifier, theory))
    1.31 +          Document.Node.Name(node, master_dir, Long_Name.qualify(qualifier, theory))
    1.32          }
    1.33      }
    1.34    }