# HG changeset patch
# User wenzelm
# Date 1568655308 -7200
# Node ID fd188463066e916586ded0f1b367aebc393a3acb
# Parent  a3cfe859d9158bb18f54aa6e9d76d3666db13225
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);

diff -r a3cfe859d915 -r fd188463066e src/Pure/PIDE/command.scala
--- 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)) +
diff -r a3cfe859d915 -r fd188463066e src/Pure/PIDE/resources.scala
--- 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 =
diff -r a3cfe859d915 -r fd188463066e src/Pure/Thy/thy_header.scala
--- 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 */