src/Pure/PIDE/resources.scala
changeset 65408 c728f922f657
parent 65392 f365f61f2081
child 65409 ad9e2c1665b6
     1.1 --- a/src/Pure/PIDE/resources.scala	Thu Apr 06 15:44:16 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Thu Apr 06 15:57:33 2017 +0200
     1.3 @@ -69,24 +69,19 @@
     1.4  
     1.5    def import_name(dir: String, s: String): Document.Node.Name =
     1.6    {
     1.7 -    val thy = Thy_Header.base_name(s)
     1.8 -    val is_global = session_base.global_theories.contains(thy)
     1.9 -    val is_qualified = Long_Name.is_qualified(thy)
    1.10 +    val theory0 = Thy_Header.base_name(s)
    1.11 +    val theory =
    1.12 +      if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
    1.13 +      else Long_Name.qualify(session_name, theory0)
    1.14  
    1.15 -    val known_theory =
    1.16 -      session_base.known_theories.get(thy) orElse
    1.17 -      (if (is_global) None
    1.18 -       else if (is_qualified) session_base.known_theories.get(Long_Name.base_name(thy))
    1.19 -       else session_base.known_theories.get(Long_Name.qualify(session_name, thy)))
    1.20 -
    1.21 -    known_theory match {
    1.22 +    session_base.known_theories.get(theory) orElse session_base.known_theories.get(theory0) match
    1.23 +    {
    1.24        case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
    1.25        case Some(name) => name
    1.26        case None =>
    1.27          val path = Path.explode(s)
    1.28          val node = append(dir, thy_path(path))
    1.29          val master_dir = append(dir, path.dir)
    1.30 -        val theory = if (is_global || is_qualified) thy else Long_Name.qualify(session_name, thy)
    1.31          Document.Node.Name(node, master_dir, theory)
    1.32      }
    1.33    }