src/Pure/Tools/imports.scala
changeset 66780 bf54ca580bf2
parent 66767 294c2e9a689e
child 66848 982baed14542
     1.1 --- a/src/Pure/Tools/imports.scala	Thu Oct 05 16:33:36 2017 +0200
     1.2 +++ b/src/Pure/Tools/imports.scala	Sat Oct 07 20:31:01 2017 +0200
     1.3 @@ -104,7 +104,7 @@
     1.4          val extra_imports =
     1.5            (for {
     1.6              (_, a) <- session_resources.session_base.known.theories.iterator
     1.7 -            if session_resources.theory_qualifier(a) == info.theory_qualifier
     1.8 +            if session_resources.theory_qualifier(a) == info.name
     1.9              b <- deps.all_known.get_file(a.path.file)
    1.10              qualifier = session_resources.theory_qualifier(b)
    1.11              if !declared_imports.contains(qualifier)
    1.12 @@ -146,14 +146,13 @@
    1.13            val updates_root =
    1.14              for {
    1.15                (_, pos) <- info.theories.flatMap(_._2)
    1.16 -              upd <- update_name(root_keywords, pos,
    1.17 -                standard_import(info.theory_qualifier, info.dir.implode, _))
    1.18 +              upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
    1.19              } yield upd
    1.20  
    1.21            val updates_theories =
    1.22              for {
    1.23                (_, name) <- session_base.known.theories_local.toList
    1.24 -              if session_resources.theory_qualifier(name) == info.theory_qualifier
    1.25 +              if session_resources.theory_qualifier(name) == info.name
    1.26                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
    1.27                upd <- update_name(session_base.overall_syntax.keywords, pos,
    1.28                  standard_import(session_resources.theory_qualifier(name), name.master_dir, _))