proper qualifier (again, see df4cd6e1fdfa);
authorwenzelm
Mon Apr 03 14:29:44 2017 +0200 (2017-04-03)
changeset 65358e345e9420109
parent 65357 9a2c266f97c8
child 65359 9ca34f0407a9
proper qualifier (again, see df4cd6e1fdfa);
src/Pure/General/long_name.ML
src/Pure/General/long_name.scala
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/General/long_name.ML	Mon Apr 03 13:39:13 2017 +0200
     1.2 +++ b/src/Pure/General/long_name.ML	Mon Apr 03 14:29:44 2017 +0200
     1.3 @@ -64,4 +64,3 @@
     1.4        in implode (nth_map (length names - 1) f names) end;
     1.5  
     1.6  end;
     1.7 -
     2.1 --- a/src/Pure/General/long_name.scala	Mon Apr 03 13:39:13 2017 +0200
     2.2 +++ b/src/Pure/General/long_name.scala	Mon Apr 03 14:29:44 2017 +0200
     2.3 @@ -25,4 +25,3 @@
     2.4      if (name == "") ""
     2.5      else explode(name).last
     2.6  }
     2.7 -
     3.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 03 13:39:13 2017 +0200
     3.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 14:29:44 2017 +0200
     3.3 @@ -24,10 +24,9 @@
     3.4  
     3.5    def node_name(qualifier: String, raw_path: Path): Document.Node.Name =
     3.6    {
     3.7 -    val no_qualifier = "" // FIXME
     3.8      val path = raw_path.expand
     3.9      val node = path.implode
    3.10 -    val theory = Long_Name.qualify(no_qualifier, Thy_Header.thy_name(node).getOrElse(""))
    3.11 +    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
    3.12      val master_dir = if (theory == "") "" else path.dir.implode
    3.13      Document.Node.Name(node, master_dir, theory)
    3.14    }
    3.15 @@ -79,9 +78,8 @@
    3.16  
    3.17    def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
    3.18    {
    3.19 -    val no_qualifier = "" // FIXME
    3.20      val thy1 = Thy_Header.base_name(s)
    3.21 -    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1)
    3.22 +    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(qualifier, thy1)
    3.23      (base.known_theories.get(thy1) orElse
    3.24       base.known_theories.get(thy2) orElse
    3.25       base.known_theories.get(Long_Name.base_name(thy1))) match {
    3.26 @@ -94,7 +92,7 @@
    3.27          else {
    3.28            val node = append(master.master_dir, thy_path(path))
    3.29            val master_dir = append(master.master_dir, path.dir)
    3.30 -          Document.Node.Name(node, master_dir, Long_Name.qualify(no_qualifier, theory))
    3.31 +          Document.Node.Name(node, master_dir, Long_Name.qualify(qualifier, theory))
    3.32          }
    3.33      }
    3.34    }