# HG changeset patch
# User wenzelm
# Date 1507214016 -7200
# Node ID 294c2e9a689e4036612ceaa442452a4b8d04e853
# Parent  19f8385ddfd3dcaf8fb74a6e962310bc5902a4d8
clarified modules;

diff -r 19f8385ddfd3 -r 294c2e9a689e src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Oct 05 14:58:04 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Oct 05 16:33:36 2017 +0200
@@ -115,6 +115,25 @@
   def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
     import_name(theory_qualifier(name), name.master_dir, s)
 
+  def standard_import(session_resources: Resources,
+    qualifier: String, dir: String, s: String): String =
+  {
+    val name = import_name(qualifier, dir, s)
+    val s1 =
+      if (session_base.loaded_theory(name)) name.theory
+      else {
+        session_base.known.get_file(name.path.file) match {
+          case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
+            name1.theory
+          case Some(name1) if Thy_Header.is_base_name(s) =>
+            name1.theory_base_name
+          case _ => s
+        }
+      }
+    val name2 = import_name(qualifier, dir, s1)
+    if (name.node == name2.node) s1 else s
+  }
+
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     val path = File.check_file(name.path)
diff -r 19f8385ddfd3 -r 294c2e9a689e src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Thu Oct 05 14:58:04 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Thu Oct 05 16:33:36 2017 +0200
@@ -141,22 +141,7 @@
           val imports_resources = new Resources(imports_base)
 
           def standard_import(qualifier: String, dir: String, s: String): String =
-          {
-            val name = imports_resources.import_name(qualifier, dir, s)
-            val s1 =
-              if (imports_base.loaded_theory(name)) name.theory
-              else {
-                imports_base.known.get_file(name.path.file) match {
-                  case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
-                    name1.theory
-                  case Some(name1) if Thy_Header.is_base_name(s) =>
-                    name1.theory_base_name
-                  case _ => s
-                }
-              }
-            val name2 = imports_resources.import_name(qualifier, dir, s1)
-            if (name.node == name2.node) s1 else s
-          }
+            imports_resources.standard_import(session_resources, qualifier, dir, s)
 
           val updates_root =
             for {