# HG changeset patch
# User wenzelm
# Date 1672777095 -3600
# Node ID d924a69e7d2b0df0a842d5635120345aa76acbae
# Parent  98993083e4ac91f539e384bd8e251f9c2e320077
more robust operations: avoid somewhat fragile Document.Node.Name.master_dir_path;

diff -r 98993083e4ac -r d924a69e7d2b src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Jan 03 20:46:56 2023 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Jan 03 21:18:15 2023 +0100
@@ -75,6 +75,13 @@
   def append_path(prefix: String, source_path: Path): String =
     File.standard_path(Path.explode(prefix) + source_path)
 
+  def read_dir(dir: String): List[String] = File.read_dir(Path.explode(dir))
+
+  def list_thys(dir: String): List[String] = {
+    val entries = try { read_dir(dir) } catch { case ERROR(_) => Nil }
+    entries.flatMap(Thy_Header.get_thy_name)
+  }
+
 
   /* source files of Isabelle/ML bootstrap */
 
@@ -192,13 +199,11 @@
 
   def complete_import_name(context_name: Document.Node.Name, s: String): List[String] = {
     val context_session = sessions_structure.theory_qualifier(context_name)
-    val context_dir =
-      try { Some(context_name.master_dir_path) }
-      catch { case ERROR(_) => None }
+    def context_dir(): List[String] = list_thys(context_name.master_dir)
+    def session_dir(info: Sessions.Info): List[String] = info.dirs.flatMap(Thy_Header.list_thys)
     (for {
       (session, (info, _)) <- sessions_structure.imports_graph.iterator
-      dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator
-      theory <- Thy_Header.list_thy_names(dir).iterator
+      theory <- (if (session == context_session) context_dir() else session_dir(info)).iterator
       if Completion.completed(s)(theory)
     } yield {
       if (session == context_session || global_theory(theory)) theory
diff -r 98993083e4ac -r d924a69e7d2b src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Jan 03 20:46:56 2023 +0100
+++ b/src/Pure/Thy/thy_header.scala	Tue Jan 03 21:18:15 2023 +0100
@@ -84,11 +84,9 @@
 
   def get_thy_name(s: String): Option[String] = Url.get_base_name(s, suffix = ".thy")
 
-  def list_thy_names(dir: Path): List[String] = {
-    val files =
-      try { File.read_dir(dir) }
-      catch { case ERROR(_) => Nil }
-    files.flatMap(get_thy_name)
+  def list_thys(dir: Path): List[String] = {
+    val entries = try { File.read_dir(dir) } catch { case ERROR(_) => Nil }
+    entries.flatMap(get_thy_name)
   }
 
   def theory_name(s: String): String =
diff -r 98993083e4ac -r d924a69e7d2b src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Jan 03 20:46:56 2023 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Jan 03 21:18:15 2023 +0100
@@ -110,6 +110,9 @@
     else File.absolute_name(new JFile(prefix + JFile.separator + File.platform_path(path)))
   }
 
+  override def read_dir(dir: String): List[String] =
+    File.read_dir(Path.explode(File.standard_path(dir)))
+
   def get_models(): Iterable[VSCode_Model] = state.value.models.values
   def get_model(file: JFile): Option[VSCode_Model] = state.value.models.get(file)
   def get_model(name: Document.Node.Name): Option[VSCode_Model] = get_model(node_file(name))
diff -r 98993083e4ac -r d924a69e7d2b src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Jan 03 20:46:56 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Jan 03 21:18:15 2023 +0100
@@ -66,6 +66,12 @@
     }
   }
 
+  override def read_dir(dir: String): List[String] = {
+    val vfs = VFSManager.getVFSForPath(dir)
+    if (vfs.isInstanceOf[FileVFS]) File.read_dir(Path.explode(File.standard_path(dir)))
+    else Nil
+  }
+
 
   /* file content */