# HG changeset patch
# User wenzelm
# Date 1751028078 -7200
# Node ID beba766806edbc9e2ed25351ae21e98923c17a01
# Parent  ec6eb16e4692bb56f1d206a00b4e7f23da35f80d
clarified signature;

diff -r ec6eb16e4692 -r beba766806ed src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Fri Jun 27 13:44:36 2025 +0200
+++ b/src/Pure/Build/build.scala	Fri Jun 27 14:41:18 2025 +0200
@@ -786,7 +786,7 @@
     metric: Pretty.Metric = Symbol.Metric,
     unicode_symbols: Boolean = false
   ): Unit = {
-    val session = new Session(options)
+    val session = new Session { override def session_options: Options = options }
     val store = session.store
 
     def check(filter: List[Regex], make_string: => String): Boolean =
diff -r ec6eb16e4692 -r beba766806ed src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Fri Jun 27 13:44:36 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Fri Jun 27 14:41:18 2025 +0200
@@ -171,7 +171,9 @@
           /* session */
 
           val session =
-            new Session(options) {
+            new Session {
+              override def session_options: Options = options
+
               override val store: Store = build_context.store
 
               override val resources: Resources =
diff -r ec6eb16e4692 -r beba766806ed src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Fri Jun 27 13:44:36 2025 +0200
+++ b/src/Pure/PIDE/headless.scala	Fri Jun 27 14:41:18 2025 +0200
@@ -47,9 +47,11 @@
     session_name: String,
     _session_options: => Options,
     _resources: Headless.Resources)
-  extends isabelle.Session(_session_options) {
+  extends isabelle.Session {
     session =>
 
+    override def session_options: Options = _session_options
+
     override def resources: Headless.Resources = _resources
 
     private def loaded_theory(name: Document.Node.Name): Boolean =
diff -r ec6eb16e4692 -r beba766806ed src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Jun 27 13:44:36 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Jun 27 14:41:18 2025 +0200
@@ -121,15 +121,17 @@
 }
 
 
-class Session(_session_options: => Options) extends Document.Session {
+abstract class Session extends Document.Session {
   session =>
 
+  def session_options: Options
+
   def resources: Resources = Resources.bootstrap
 
   val init_time: Time = Time.now()
   def print_now(): String = (Time.now() - init_time).toString
 
-  val store: Store = Store(_session_options)
+  val store: Store = Store(session_options)
   def cache: Rich_Text.Cache = store.cache
 
   def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.empty
@@ -154,8 +156,6 @@
 
   /* dynamic session options */
 
-  def session_options: Options = _session_options
-
   def load_delay: Time = session_options.seconds("editor_load_delay")
   def input_delay: Time = session_options.seconds("editor_input_delay")
   def generated_input_delay: Time = session_options.seconds("editor_generated_input_delay")
diff -r ec6eb16e4692 -r beba766806ed src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Fri Jun 27 13:44:36 2025 +0200
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Fri Jun 27 14:41:18 2025 +0200
@@ -627,7 +627,7 @@
   ): Unit = {
     val solr = Solr.init(solr_data_dir)
     val database = options.string("find_facts_database_name")
-    val session = Session(options)
+    val session = new Session { override def session_options: Options = options }
 
     val selection = Sessions.Selection(sessions = sessions)
     val sessions_structure =
diff -r ec6eb16e4692 -r beba766806ed src/Tools/VSCode/src/vscode_session.scala
--- a/src/Tools/VSCode/src/vscode_session.scala	Fri Jun 27 13:44:36 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_session.scala	Fri Jun 27 14:41:18 2025 +0200
@@ -13,6 +13,7 @@
 class VSCode_Session(
   _session_options: => Options,
   _resources: VSCode_Resources
-) extends Session(_session_options) {
+) extends Session {
+  override def session_options: Options = _session_options
   override def resources: VSCode_Resources = _resources
 }
diff -r ec6eb16e4692 -r beba766806ed src/Tools/jEdit/src/jedit_session.scala
--- a/src/Tools/jEdit/src/jedit_session.scala	Fri Jun 27 13:44:36 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_session.scala	Fri Jun 27 14:41:18 2025 +0200
@@ -161,9 +161,10 @@
   }
 }
 
-class JEdit_Session(_session_options: => Options) extends Session(_session_options) {
-  override val resources: JEdit_Resources = JEdit_Resources(_session_options)
-  override val store: Store = Store(JEdit_Session.session_options(_session_options))
+class JEdit_Session(_session_options: => Options) extends Session {
+  override def session_options: Options = _session_options
+  override val resources: JEdit_Resources = JEdit_Resources(session_options)
+  override val store: Store = Store(JEdit_Session.session_options(session_options))
 
   override def auto_resolve: Boolean = session_options.bool("jedit_auto_resolve")
 }