clarified import of loaded theory;
authorwenzelm
Tue Jun 06 23:13:53 2017 +0200 (2017-06-06)
changeset 6602596f86c613a9f
parent 66024 77d9334830ec
child 66026 704e4970d703
child 66027 396785562768
clarified import of loaded theory;
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/Tools/imports.scala	Mon Jun 05 21:24:41 2017 +0200
     1.2 +++ b/src/Pure/Tools/imports.scala	Tue Jun 06 23:13:53 2017 +0200
     1.3 @@ -141,14 +141,16 @@
     1.4            def standard_import(qualifier: String, dir: String, s: String): String =
     1.5            {
     1.6              val name = imports_resources.import_name(qualifier, dir, s)
     1.7 -            val file = Path.explode(name.node).file
     1.8              val s1 =
     1.9 -              imports_resources.session_base.known.get_file(file) match {
    1.10 -                case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    1.11 -                  name1.theory
    1.12 -                case Some(name1) if Thy_Header.is_base_name(s) =>
    1.13 -                  name1.theory_base_name
    1.14 -                case _ => s
    1.15 +              if (session_base.loaded_theory(name)) name.theory
    1.16 +              else {
    1.17 +                imports_resources.session_base.known.get_file(Path.explode(name.node).file) match {
    1.18 +                  case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    1.19 +                    name1.theory
    1.20 +                  case Some(name1) if Thy_Header.is_base_name(s) =>
    1.21 +                    name1.theory_base_name
    1.22 +                  case _ => s
    1.23 +                }
    1.24                }
    1.25              val name2 = imports_resources.import_name(qualifier, dir, s1)
    1.26              if (name.node == name2.node) s1 else s