src/Pure/PIDE/resources.scala
changeset 65471 05e5bffcf1d8
parent 65467 9535c670b1b4
child 65472 f83081bcdd0e
     1.1 --- a/src/Pure/PIDE/resources.scala	Wed Apr 12 21:13:43 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Wed Apr 12 22:32:55 2017 +0200
     1.3 @@ -70,23 +70,30 @@
     1.4    def theory_qualifier(name: Document.Node.Name): String =
     1.5      session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
     1.6  
     1.7 +  def theory_name(qualifier: String, theory0: String): (Boolean, String) =
     1.8 +    session_base.loaded_theories.get(theory0) match {
     1.9 +      case Some(theory) => (true, theory)
    1.10 +      case None =>
    1.11 +        val theory =
    1.12 +          if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0)
    1.13 +              || true /* FIXME */) theory0
    1.14 +          else Long_Name.qualify(qualifier, theory0)
    1.15 +        (false, theory)
    1.16 +    }
    1.17 +
    1.18    def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
    1.19    {
    1.20 -    val theory0 = Thy_Header.import_name(s)
    1.21 -    val theory =
    1.22 -      if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0)
    1.23 -        || true /* FIXME */) theory0
    1.24 -      else Long_Name.qualify(qualifier, theory0)
    1.25 -
    1.26 -    session_base.loaded_theories.get(theory) orElse
    1.27 -    session_base.loaded_theories.get(theory0) orElse
    1.28 -    session_base.known_theories.get(theory) orElse
    1.29 -    session_base.known_theories.get(theory0) getOrElse {
    1.30 -      val path = Path.explode(s)
    1.31 -      val node = append(dir, thy_path(path))
    1.32 -      val master_dir = append(dir, path.dir)
    1.33 -      Document.Node.Name(node, master_dir, theory)
    1.34 -    }
    1.35 +    val (loaded, theory) = theory_name(qualifier, Thy_Header.import_name(s))
    1.36 +    if (loaded) Document.Node.Name.loaded_theory(theory)
    1.37 +    else
    1.38 +      session_base.known_theories.get(theory) match {
    1.39 +        case Some(node_name) => node_name
    1.40 +        case None =>
    1.41 +          val path = Path.explode(s)
    1.42 +          val node = append(dir, thy_path(path))
    1.43 +          val master_dir = append(dir, path.dir)
    1.44 +          Document.Node.Name(node, master_dir, theory)
    1.45 +      }
    1.46    }
    1.47  
    1.48    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =