more standard master_dir;
authorwenzelm
Fri, 21 Apr 2017 15:00:31 +0200
changeset 65533 4a7e794944df
parent 65532 febfd9f78bd4
child 65534 b6250ee6ce79
more standard master_dir;
src/Pure/Tools/update_imports.scala
--- a/src/Pure/Tools/update_imports.scala	Fri Apr 21 14:09:03 2017 +0200
+++ b/src/Pure/Tools/update_imports.scala	Fri Apr 21 15:00:31 2017 +0200
@@ -71,9 +71,9 @@
       val resources = new Resources(session_base)
       val local_theories = session_base.known.theories_local.iterator.map(_._2).toSet
 
-      def standard_import(qualifier: String, s: String): String =
+      def standard_import(qualifier: String, dir: String, s: String): String =
       {
-        val name = resources.import_name(qualifier, "", s)
+        val name = resources.import_name(qualifier, dir, s)
         if (!local_theories.contains(name)) s
         if (resources.theory_qualifier(name) != qualifier) name.theory
         else if (Thy_Header.is_base_name(s)) name.theory_base_name
@@ -84,7 +84,7 @@
         for {
           (_, pos) <- info.theories.flatMap(_._2)
           upd <- update_name(Sessions.root_syntax.keywords, pos,
-            standard_import(info.theory_qualifier, _))
+            standard_import(info.theory_qualifier, info.dir.implode, _))
         } yield upd
 
       val updates_theories =
@@ -96,7 +96,7 @@
               Scan.char_reader(File.read(Path.explode(name.node))),
               Token.Pos.file(name.node)).imports
           upd <- update_name(session_base.syntax.keywords, pos,
-            standard_import(resources.theory_qualifier(name), _))
+            standard_import(resources.theory_qualifier(name), name.master_dir, _))
         } yield upd
 
       updates_root ::: updates_theories