# HG changeset patch
# User wenzelm
# Date 1509474564 -3600
# Node ID f3f9a492bee66b504ecb03ca63e43164986e63bc
# Parent  9cec5035409944bdc404efec242bbb65fe25217a
clarified signature;

diff -r 9cec50354099 -r f3f9a492bee6 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Oct 31 18:56:24 2017 +0100
+++ b/src/Pure/PIDE/command.scala	Tue Oct 31 19:29:24 2017 +0100
@@ -452,12 +452,16 @@
             val completion =
               if (Thy_Header.is_base_name(s)) {
                 val completed = Completion.completed(import_name.theory_base_name)
-                val qualifier = resources.theory_qualifier(node_name)
+                val qualifier = resources.session_base.theory_qualifier(node_name)
                 val dir = node_name.master_dir
                 for {
                   (_, known_name) <- resources.session_base.known.theories.toList
                   if completed(known_name.theory_base_name)
-                } yield resources.standard_import(resources, qualifier, dir, known_name.theory)
+                }
+                yield {
+                  resources.standard_import(
+                    resources.session_base, qualifier, dir, known_name.theory)
+                }
               }.sorted
               else Nil
             val msg =
diff -r 9cec50354099 -r f3f9a492bee6 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Oct 31 18:56:24 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Oct 31 19:29:24 2017 +0100
@@ -86,9 +86,6 @@
     roots ::: files
   }
 
-  def theory_qualifier(name: Document.Node.Name): String =
-    session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
-
   def theory_name(qualifier: String, theory: String): (Boolean, String) =
     if (session_base.loaded_theory(theory)) (true, theory)
     else {
@@ -118,10 +115,9 @@
     }
 
   def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
-    import_name(theory_qualifier(name), name.master_dir, s)
+    import_name(session_base.theory_qualifier(name), name.master_dir, s)
 
-  def standard_import(session_resources: Resources,
-    qualifier: String, dir: String, s: String): String =
+  def standard_import(base: Sessions.Base, qualifier: String, dir: String, s: String): String =
   {
     val name = import_name(qualifier, dir, s)
     val s1 =
@@ -131,7 +127,7 @@
           case None => s
           case Some(path) =>
             session_base.known.get_file(path.file) match {
-              case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
+              case Some(name1) if base.theory_qualifier(name1) != qualifier =>
                 name1.theory
               case Some(name1) if Thy_Header.is_base_name(s) =>
                 name1.theory_base_name
diff -r 9cec50354099 -r f3f9a492bee6 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Oct 31 18:56:24 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 19:29:24 2017 +0100
@@ -123,6 +123,9 @@
     def platform_path: Base = copy(known = known.platform_path)
     def standard_path: Base = copy(known = known.standard_path)
 
+    def theory_qualifier(name: Document.Node.Name): String =
+      global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
+
     def loaded_theory(name: String): Boolean = loaded_theories.defined(name)
     def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
 
@@ -260,7 +263,7 @@
 
               def node(name: Document.Node.Name): Graph_Display.Node =
               {
-                val qualifier = resources.theory_qualifier(name)
+                val qualifier = imports_base.theory_qualifier(name)
                 if (qualifier == info.name)
                   Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
                 else session_node(qualifier)
diff -r 9cec50354099 -r f3f9a492bee6 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Tue Oct 31 18:56:24 2017 +0100
+++ b/src/Pure/Tools/imports.scala	Tue Oct 31 19:29:24 2017 +0100
@@ -113,24 +113,23 @@
       {
         val info = selected_sessions(session_name)
         val session_base = deps(session_name)
-        val session_resources = new Resources(session_base)
 
         val declared_imports =
           selected_sessions.imports_requirements(List(session_name)).toSet
 
         val extra_imports =
           (for {
-            (_, a) <- session_resources.session_base.known.theories.iterator
-            if session_resources.theory_qualifier(a) == info.name
+            (_, a) <- session_base.known.theories.iterator
+            if session_base.theory_qualifier(a) == info.name
             b <- deps.all_known.get_file(a.path.file)
-            qualifier = session_resources.theory_qualifier(b)
+            qualifier = session_base.theory_qualifier(b)
             if !declared_imports.contains(qualifier)
           } yield qualifier).toSet
 
         val loaded_imports =
           selected_sessions.imports_requirements(
             session_base.loaded_theories.keys.map(a =>
-              session_resources.theory_qualifier(session_base.known.theories(a))))
+              session_base.theory_qualifier(session_base.known.theories(a))))
           .toSet - session_name
 
         val minimal_imports =
@@ -182,7 +181,7 @@
           val imports_resources = new Resources(imports_base)
 
           def standard_import(qualifier: String, dir: String, s: String): String =
-            imports_resources.standard_import(session_resources, qualifier, dir, s)
+            imports_resources.standard_import(session_base, qualifier, dir, s)
 
           val updates_root =
             for {
@@ -193,10 +192,10 @@
           val updates_theories =
             for {
               (_, name) <- session_base.known.theories_local.toList
-              if session_resources.theory_qualifier(name) == info.name
+              if session_base.theory_qualifier(name) == info.name
               (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
               upd <- update_name(session_base.overall_syntax.keywords, pos,
-                standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
+                standard_import(session_base.theory_qualifier(name), name.master_dir, _))
             } yield upd
 
           updates_root ::: updates_theories