src/Pure/Tools/imports.scala
changeset 66716 8737b866bd1c
parent 66671 41b64e53b6a1
child 66720 b07192253605
     1.1 --- a/src/Pure/Tools/imports.scala	Fri Sep 29 17:35:09 2017 +0200
     1.2 +++ b/src/Pure/Tools/imports.scala	Fri Sep 29 17:41:39 2017 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4            (for {
     1.5              (_, a) <- session_resources.session_base.known.theories.iterator
     1.6              if session_resources.theory_qualifier(a) == info.theory_qualifier
     1.7 -            b <- deps.all_known.get_file(Path.explode(a.node).file)
     1.8 +            b <- deps.all_known.get_file(a.path.file)
     1.9              qualifier = session_resources.theory_qualifier(b)
    1.10              if !declared_imports.contains(qualifier)
    1.11            } yield qualifier).toSet
    1.12 @@ -146,7 +146,7 @@
    1.13              val s1 =
    1.14                if (imports_base.loaded_theory(name)) name.theory
    1.15                else {
    1.16 -                imports_base.known.get_file(Path.explode(name.node).file) match {
    1.17 +                imports_base.known.get_file(name.path.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) =>