clarified signature: avoid Session with accidental Resources.bootstrap, which is mostly undefined;
--- 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 =
--- 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
--- 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 =