no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;
authorwenzelm
Thu May 08 16:19:16 2014 +0200 (2014-05-08)
changeset 56913df4cd6e1fdfa
parent 56912 293cd4dcfebc
child 56914 f371418b9641
no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Thu May 08 16:15:20 2014 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Thu May 08 16:19:16 2014 +0200
     1.3 @@ -28,9 +28,10 @@
     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(qualifier, Thy_Header.thy_name(node).getOrElse(""))
    1.11 +    val theory = Long_Name.qualify(no_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 @@ -65,8 +66,9 @@
    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(qualifier, thy1)
    1.22 +    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1)
    1.23      (known_theories.get(thy1) orElse
    1.24       known_theories.get(thy2) orElse
    1.25       known_theories.get(Long_Name.base_name(thy1))) match {
    1.26 @@ -79,7 +81,7 @@
    1.27          else {
    1.28            val node = append(master.master_dir, Resources.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(qualifier, theory))
    1.31 +          Document.Node.Name(node, master_dir, Long_Name.qualify(no_qualifier, theory))
    1.32          }
    1.33      }
    1.34    }