# HG changeset patch
# User wenzelm
# Date 1672758857 -3600
# Node ID c2932487360dd7d45d00a149c330a5b079b57e38
# Parent  a004c5322ea4402cb9edf2841afd1b91c06e701f
tuned;

diff -r a004c5322ea4 -r c2932487360d src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Jan 03 16:05:07 2023 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Jan 03 16:14:17 2023 +0100
@@ -127,15 +127,13 @@
       yield (dir + Path.explode(file)).expand
   }
 
-  def pure_files(syntax: Outer_Syntax): List[Path] = {
-    val pure_dir = Path.explode("~~/src/Pure")
-    for {
-      (name, theory) <- Thy_Header.ml_roots
-      path = (pure_dir + Path.explode(name)).expand
-      node_name = Document.Node.Name(path.implode, theory = theory)
-      file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)())
-    } yield file
-  }
+  def pure_files(syntax: Outer_Syntax): List[Path] =
+    (for {
+      (name, theory) <- Thy_Header.ml_roots.iterator
+      node = append_path("~~/src/Pure", Path.explode(name))
+      node_name = Document.Node.Name(node, theory = theory)
+      file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)()).iterator
+    } yield file).toList
 
   def global_theory(theory: String): Boolean =
     sessions_structure.global_theories.isDefinedAt(theory)