src/Pure/PIDE/resources.scala
changeset 65362 908a27a4b9c9
parent 65361 ecefb68dc21d
child 65368 7fb5aad28f38
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 03 17:00:36 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 21:17:47 2017 +0200
     1.3 @@ -79,22 +79,26 @@
     1.4  
     1.5    def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
     1.6    {
     1.7 -    val thy1 = Thy_Header.base_name(s)
     1.8 -    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(session_name, thy1)
     1.9 -    (session_base.known_theories.get(thy1) orElse
    1.10 -     session_base.known_theories.get(thy2) orElse
    1.11 -     session_base.known_theories.get(Long_Name.base_name(thy1))) match {
    1.12 +    val theory = Thy_Header.base_name(s)
    1.13 +    val is_base_name = Thy_Header.is_base_name(s)
    1.14 +    val is_qualified = is_base_name && Long_Name.is_qualified(s)
    1.15 +
    1.16 +    val known_theory =
    1.17 +      if (is_base_name)
    1.18 +        session_base.known_theories.get(theory) orElse
    1.19 +        (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
    1.20 +         else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
    1.21 +      else None
    1.22 +
    1.23 +    known_theory match {
    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 if is_qualified => Document.Node.Name.theory(theory)
    1.27        case None =>
    1.28          val path = Path.explode(s)
    1.29 -        val theory = path.base.implode
    1.30 -        if (Long_Name.is_qualified(theory)) Document.Node.Name.theory(theory)
    1.31 -        else {
    1.32 -          val node = append(master.master_dir, thy_path(path))
    1.33 -          val master_dir = append(master.master_dir, path.dir)
    1.34 -          Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory))
    1.35 -        }
    1.36 +        val node = append(master.master_dir, thy_path(path))
    1.37 +        val master_dir = append(master.master_dir, path.dir)
    1.38 +        Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory))
    1.39      }
    1.40    }
    1.41