more standard master_dir;
authorwenzelm
Fri Apr 21 15:00:31 2017 +0200 (2017-04-21 ago)
changeset 655334a7e794944df
parent 65532 febfd9f78bd4
child 65534 b6250ee6ce79
more standard master_dir;
src/Pure/Tools/update_imports.scala
     1.1 --- a/src/Pure/Tools/update_imports.scala	Fri Apr 21 14:09:03 2017 +0200
     1.2 +++ b/src/Pure/Tools/update_imports.scala	Fri Apr 21 15:00:31 2017 +0200
     1.3 @@ -71,9 +71,9 @@
     1.4        val resources = new Resources(session_base)
     1.5        val local_theories = session_base.known.theories_local.iterator.map(_._2).toSet
     1.6  
     1.7 -      def standard_import(qualifier: String, s: String): String =
     1.8 +      def standard_import(qualifier: String, dir: String, s: String): String =
     1.9        {
    1.10 -        val name = resources.import_name(qualifier, "", s)
    1.11 +        val name = resources.import_name(qualifier, dir, s)
    1.12          if (!local_theories.contains(name)) s
    1.13          if (resources.theory_qualifier(name) != qualifier) name.theory
    1.14          else if (Thy_Header.is_base_name(s)) name.theory_base_name
    1.15 @@ -84,7 +84,7 @@
    1.16          for {
    1.17            (_, pos) <- info.theories.flatMap(_._2)
    1.18            upd <- update_name(Sessions.root_syntax.keywords, pos,
    1.19 -            standard_import(info.theory_qualifier, _))
    1.20 +            standard_import(info.theory_qualifier, info.dir.implode, _))
    1.21          } yield upd
    1.22  
    1.23        val updates_theories =
    1.24 @@ -96,7 +96,7 @@
    1.25                Scan.char_reader(File.read(Path.explode(name.node))),
    1.26                Token.Pos.file(name.node)).imports
    1.27            upd <- update_name(session_base.syntax.keywords, pos,
    1.28 -            standard_import(resources.theory_qualifier(name), _))
    1.29 +            standard_import(resources.theory_qualifier(name), name.master_dir, _))
    1.30          } yield upd
    1.31  
    1.32        updates_root ::: updates_theories