# HG changeset patch
# User wenzelm
# Date 1492779631 -7200
# Node ID 4a7e794944df5b5eaae5cc8dce5e7a7fa020f69d
# Parent  febfd9f78bd408c617dd90d1c3a05d52e1ac2be7
more standard master_dir;

diff -r febfd9f78bd4 -r 4a7e794944df 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