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