tuned;
authorwenzelm
Wed Jun 07 19:13:22 2017 +0200 (2017-06-07)
changeset 6602814c014a43278
parent 66027 396785562768
child 66029 063f13f10433
tuned;
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/Tools/imports.scala	Wed Jun 07 15:52:18 2017 +0200
     1.2 +++ b/src/Pure/Tools/imports.scala	Wed Jun 07 19:13:22 2017 +0200
     1.3 @@ -136,7 +136,8 @@
     1.4            val info = full_sessions(session_name)
     1.5            val session_base = deps(session_name)
     1.6            val session_resources = new Resources(session_base)
     1.7 -          val imports_resources = new Resources(session_base.get_imports)
     1.8 +          val imports_base = session_base.get_imports
     1.9 +          val imports_resources = new Resources(imports_base)
    1.10  
    1.11            def standard_import(qualifier: String, dir: String, s: String): String =
    1.12            {
    1.13 @@ -144,7 +145,7 @@
    1.14              val s1 =
    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 +                imports_base.known.get_file(Path.explode(name.node).file) match {
    1.19                    case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    1.20                      name1.theory
    1.21                    case Some(name1) if Thy_Header.is_base_name(s) =>