# HG changeset patch
# User wenzelm
# Date 1751029392 -7200
# Node ID 0751d363fd0e8fb204e04233bbcf8a4a685691bc
# Parent  98d9abefd9b046e6cbdfbf481e14d7f2ebab0ca9
clarified signature: avoid Session with accidental Resources.bootstrap, which is mostly undefined;

diff -r 98d9abefd9b0 -r 0751d363fd0e src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Fri Jun 27 14:52:01 2025 +0200
+++ b/src/Pure/Build/build.scala	Fri Jun 27 15:03:12 2025 +0200
@@ -786,7 +786,7 @@
     metric: Pretty.Metric = Symbol.Metric,
     unicode_symbols: Boolean = false
   ): Unit = {
-    val session = new Session { override def session_options: Options = options }
+    val session = Session.bootstrap(options)
     val store = session.store
 
     def check(filter: List[Regex], make_string: => String): Boolean =
diff -r 98d9abefd9b0 -r 0751d363fd0e src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Jun 27 14:52:01 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Jun 27 15:03:12 2025 +0200
@@ -118,6 +118,15 @@
     def functions: Protocol_Functions = Nil
     def prover_options(options: Options): Options = options
   }
+
+
+  /* bootstrap session */
+
+  def bootstrap(options: Options): Session =
+    new Session {
+      override def session_options: Options = options
+      override def resources: Resources = Resources.bootstrap
+    }
 }
 
 
@@ -125,8 +134,7 @@
   session =>
 
   def session_options: Options
-
-  def resources: Resources = Resources.bootstrap
+  def resources: Resources
 
   val store: Store = Store(session_options)
   def cache: Rich_Text.Cache = store.cache
diff -r 98d9abefd9b0 -r 0751d363fd0e src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Fri Jun 27 14:52:01 2025 +0200
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Fri Jun 27 15:03:12 2025 +0200
@@ -627,7 +627,7 @@
   ): Unit = {
     val solr = Solr.init(solr_data_dir)
     val database = options.string("find_facts_database_name")
-    val session = new Session { override def session_options: Options = options }
+    val session = Session.bootstrap(options)
 
     val selection = Sessions.Selection(sessions = sessions)
     val sessions_structure =