clarified modules;

--- a/src/Pure/Build/resources.scala	Wed Jun 25 11:46:08 2025 +0200
+++ b/src/Pure/Build/resources.scala	Wed Jun 25 11:51:13 2025 +0200
@@ -80,30 +80,6 @@
   }
 
 
-  /* source files of Isabelle/ML bootstrap */
-
-  def source_file(ml_settings: ML_Settings, raw_name: String): Option[String] = {
-    if (Path.is_wellformed(raw_name)) {
-      if (Path.is_valid(raw_name)) {
-        def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
-
-        val path = Path.explode(raw_name)
-        val path1 =
-          if (path.is_absolute || path.is_current) check(path)
-          else {
-            check(Path.explode("~~/src/Pure") + path) orElse {
-              val ml_sources = ml_settings.ml_sources
-              if (ml_sources.is_dir) check(ml_sources + path) else None
-            }
-          }
-        Some(File.platform_path(path1 getOrElse path))
-      }
-      else None
-    }
-    else Some(raw_name)
-  }
-
-
   /* theory files */
 
   def load_commands(

--- a/src/Pure/Build/store.scala	Wed Jun 25 11:46:08 2025 +0200
+++ b/src/Pure/Build/store.scala	Wed Jun 25 11:51:13 2025 +0200
@@ -295,6 +295,30 @@
     Path.variable("ISABELLE_HEAPS") + Path.basic(ml_settings.ml_identifier)
 
 
+  /* source files of Isabelle/ML bootstrap */
+
+  def source_file(raw_name: String): Option[String] = {
+    if (Path.is_wellformed(raw_name)) {
+      if (Path.is_valid(raw_name)) {
+        def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
+
+        val path = Path.explode(raw_name)
+        val path1 =
+          if (path.is_absolute || path.is_current) check(path)
+          else {
+            check(Path.explode("~~/src/Pure") + path) orElse {
+              val ml_sources = ml_settings.ml_sources
+              if (ml_sources.is_dir) check(ml_sources + path) else None
+            }
+          }
+        Some(File.platform_path(path1 getOrElse path))
+      }
+      else None
+    }
+    else Some(raw_name)
+  }
+
+
   /* directories */
 
   def system_heaps: Boolean = options.bool("system_heaps")

--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Wed Jun 25 11:46:08 2025 +0200
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Wed Jun 25 11:51:13 2025 +0200
@@ -53,7 +53,7 @@
               for {
                 thy_file <- Position.Def_File.unapply(props)
                 def_line <- Position.Def_Line.unapply(props)
-                platform_path <- resources.source_file(session.store.ml_settings, thy_file)
+                platform_path <- session.store.source_file(thy_file)
                 uri = File.uri(Path.explode(File.standard_path(platform_path)).absolute_file)
               } yield HTML.link(uri.toString + "#" + def_line, body)
           }

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jun 25 11:46:08 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jun 25 11:51:13 2025 +0200
@@ -264,7 +264,7 @@
     range: Symbol.Range
   ): Option[Line.Node_Range] = {
     for {
-      platform_path <- resources.source_file(model.session.store.ml_settings, source_name)
+      platform_path <- model.session.store.source_file(source_name)
       file <-
         (try { Some(File.absolute(new JFile(platform_path))) }
          catch { case ERROR(_) => None })

--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jun 25 11:46:08 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Jun 25 11:51:13 2025 +0200
@@ -220,7 +220,7 @@
     line1: Int,
     offset: Symbol.Offset
   ) : Option[Hyperlink] = {
-    for (platform_path <- PIDE.resources.source_file(PIDE.ml_settings, source_name)) yield {
+    for (platform_path <- PIDE.session.store.source_file(source_name)) yield {
       def hyperlink(pos: Line.Position) =
         hyperlink_file(focus, platform_path, line = pos.line, offset = pos.column)