# HG changeset patch
# User wenzelm
# Date 1492793484 -7200
# Node ID 2b73ed8bf4d96a44a1c9551ef278edfe295c8218
# Parent  dbcd9b3e1b49d5a506cdd3c0b848282098d2a59e
proper imports_resources for import_name: avoid self-referential name resolution;

diff -r dbcd9b3e1b49 -r 2b73ed8bf4d9 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Apr 21 17:34:13 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 21 18:51:24 2017 +0200
@@ -98,6 +98,7 @@
   }
 
   sealed case class Base(
+    imports: Option[Base] = None,
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Map[String, String] = Map.empty,
     known: Known = Known.empty,
@@ -106,6 +107,8 @@
     sources: List[(Path, SHA1.Digest)] = Nil,
     session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
   {
+    def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
+
     def platform_path: Base = copy(known = known.platform_path)
 
     def loaded_theory(name: Document.Node.Name): Boolean =
@@ -237,7 +240,8 @@
             }
 
             val base =
-              Base(global_theories = global_theories,
+              Base(imports = Some(imports_base),
+                global_theories = global_theories,
                 loaded_theories = thy_deps.loaded_theories,
                 known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
                 keywords = thy_deps.keywords,
diff -r dbcd9b3e1b49 -r 2b73ed8bf4d9 src/Pure/Tools/update_imports.scala
--- a/src/Pure/Tools/update_imports.scala	Fri Apr 21 17:34:13 2017 +0200
+++ b/src/Pure/Tools/update_imports.scala	Fri Apr 21 18:51:24 2017 +0200
@@ -68,22 +68,24 @@
     {
       val info = full_sessions(session_name)
       val session_base = deps(session_name)
-      val resources = new Resources(session_base)
+      val session_resources = new Resources(session_base)
+      val imports_resources = new Resources(session_base.get_imports)
+
       val local_theories =
         (for {
           (_, name) <- session_base.known.theories_local.iterator
-          if resources.theory_qualifier(name) == info.theory_qualifier
+          if session_resources.theory_qualifier(name) == info.theory_qualifier
         } yield name).toSet
 
       def standard_import(qualifier: String, dir: String, s: String): String =
       {
-        val name = resources.import_name(qualifier, dir, s)
+        val name = imports_resources.import_name(qualifier, dir, s)
         val s1 =
           if (!local_theories.contains(name)) s
-          else if (resources.theory_qualifier(name) != qualifier) name.theory
+          else if (session_resources.theory_qualifier(name) != qualifier) name.theory
           else if (Thy_Header.is_base_name(s)) name.theory_base_name
           else s
-        val name1 = resources.import_name(qualifier, dir, s1)
+        val name1 = imports_resources.import_name(qualifier, dir, s1)
         if (name == name1) s1 else s
       }
 
@@ -97,9 +99,9 @@
       val updates_theories =
         for {
           (_, name) <- session_base.known.theories_local.toList
-          (_, pos) <- resources.check_thy(name, Token.Pos.file(name.node)).imports
+          (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
           upd <- update_name(session_base.syntax.keywords, pos,
-            standard_import(resources.theory_qualifier(name), name.master_dir, _))
+            standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
         } yield upd
 
       updates_root ::: updates_theories