--- 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)
--- 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 {