src/Pure/PIDE/resources.scala
changeset 66767 294c2e9a689e
parent 66766 19f8385ddfd3
child 66771 925d10a7a610
     1.1 --- a/src/Pure/PIDE/resources.scala	Thu Oct 05 14:58:04 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Thu Oct 05 16:33:36 2017 +0200
     1.3 @@ -115,6 +115,25 @@
     1.4    def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
     1.5      import_name(theory_qualifier(name), name.master_dir, s)
     1.6  
     1.7 +  def standard_import(session_resources: Resources,
     1.8 +    qualifier: String, dir: String, s: String): String =
     1.9 +  {
    1.10 +    val name = import_name(qualifier, dir, s)
    1.11 +    val s1 =
    1.12 +      if (session_base.loaded_theory(name)) name.theory
    1.13 +      else {
    1.14 +        session_base.known.get_file(name.path.file) match {
    1.15 +          case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    1.16 +            name1.theory
    1.17 +          case Some(name1) if Thy_Header.is_base_name(s) =>
    1.18 +            name1.theory_base_name
    1.19 +          case _ => s
    1.20 +        }
    1.21 +      }
    1.22 +    val name2 = import_name(qualifier, dir, s1)
    1.23 +    if (name.node == name2.node) s1 else s
    1.24 +  }
    1.25 +
    1.26    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.27    {
    1.28      val path = File.check_file(name.path)