clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
--- a/src/Pure/PIDE/command.scala Mon Sep 16 16:00:10 2019 +0200
+++ b/src/Pure/PIDE/command.scala Mon Sep 16 19:35:08 2019 +0200
@@ -524,20 +524,7 @@
for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
yield {
val completion =
- if (Thy_Header.is_base_name(s)) {
- val completed = Completion.completed(import_name.theory_base_name)
- val qualifier = resources.session_base.theory_qualifier(node_name)
- val dir = node_name.master_dir
- for {
- known_name <- resources.session_base.known.theory_names
- if completed(known_name.theory_base_name)
- }
- yield {
- resources.standard_import(
- resources.session_base, qualifier, dir, known_name.theory)
- }
- }.sorted
- else Nil
+ if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
val msg =
"Bad theory import " +
Markup.Path(import_name.node).markup(quote(import_name.toString)) +
--- a/src/Pure/PIDE/resources.scala Mon Sep 16 16:00:10 2019 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Sep 16 19:35:08 2019 +0200
@@ -168,26 +168,21 @@
(thy, _) <- thys.iterator
} yield import_name(info, thy)).toSet
- def standard_import(base: Sessions.Base, qualifier: String, dir: String, s: String): String =
+ def complete_import_name(context_name: Document.Node.Name, s: String): List[String] =
{
- val name = import_name(qualifier, dir, s)
- val s1 =
- if (session_base.loaded_theory(name)) name.theory
- else {
- (try { Some(name.path) } catch { case ERROR(_) => None }) match {
- case None => s
- case Some(path) =>
- session_base.known.get_file(path.file) match {
- 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
- case _ => s
- }
- }
- }
- val name2 = import_name(qualifier, dir, s1)
- if (name.node == name2.node) s1 else s
+ val context_session = session_base.theory_qualifier(context_name)
+ val context_dir =
+ try { Some(context_name.master_dir_path) }
+ catch { case ERROR(_) => None }
+ (for {
+ (session, (info, _)) <- sessions_structure.imports_graph.iterator
+ dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator
+ theory <- Thy_Header.try_read_dir(dir).iterator
+ if Completion.completed(s)(theory)
+ } yield {
+ if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory
+ else Long_Name.qualify(session, theory)
+ }).toList.sorted
}
def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
--- a/src/Pure/Thy/thy_header.scala Mon Sep 16 16:00:10 2019 +0200
+++ b/src/Pure/Thy/thy_header.scala Mon Sep 16 19:35:08 2019 +0200
@@ -116,6 +116,14 @@
def bootstrap_name(theory: String): String =
bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
+ def try_read_dir(dir: Path): List[String] =
+ {
+ val files =
+ try { File.read_dir(dir) }
+ catch { case ERROR(_) => Nil }
+ for { Thy_File_Name(name) <- files } yield name
+ }
+
/* parser */