# HG changeset patch
# User wenzelm
# Date 1750791129 -7200
# Node ID 0ca8b1861fa30a646bd0c376c2680cef1073b6e3
# Parent  b00337cda5b9e01b149fe31ffd98b5255c0d2961
clarified signature: more explicit subtypes of Session, with corresponding subtypes of Resources;

diff -r b00337cda5b9 -r 0ca8b1861fa3 etc/build.props
--- a/etc/build.props	Mon Jun 23 14:44:59 2025 +0200
+++ b/etc/build.props	Tue Jun 24 20:52:09 2025 +0200
@@ -288,6 +288,7 @@
   src/Tools/VSCode/src/vscode_model.scala \
   src/Tools/VSCode/src/vscode_rendering.scala \
   src/Tools/VSCode/src/vscode_resources.scala \
+  src/Tools/VSCode/src/vscode_session.scala \
   src/Tools/VSCode/src/vscode_spell_checker.scala \
   src/Tools/jEdit/src/active.scala \
   src/Tools/jEdit/src/base_plugin.scala \
@@ -318,6 +319,7 @@
   src/Tools/jEdit/src/jedit_plugins.scala \
   src/Tools/jEdit/src/jedit_rendering.scala \
   src/Tools/jEdit/src/jedit_resources.scala \
+  src/Tools/jEdit/src/jedit_session.scala \
   src/Tools/jEdit/src/jedit_sessions.scala \
   src/Tools/jEdit/src/jedit_spell_checker.scala \
   src/Tools/jEdit/src/keymap_merge.scala \
diff -r b00337cda5b9 -r 0ca8b1861fa3 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Mon Jun 23 14:44:59 2025 +0200
+++ b/src/Pure/Build/build.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -787,7 +787,7 @@
     unicode_symbols: Boolean = false
   ): Unit = {
     val store = Store(options)
-    val session = new Session(options, Resources.bootstrap)
+    val session = new Session(options)
 
     def check(filter: List[Regex], make_string: => String): Boolean =
       filter.isEmpty || {
diff -r b00337cda5b9 -r 0ca8b1861fa3 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Mon Jun 23 14:44:59 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -170,13 +170,14 @@
 
           /* session */
 
-          val resources =
-            new Resources(session_background, log = log,
-              command_timings =
-                Properties.uncompress(session_context.old_command_timings_blob, cache = store.cache))
+          val session =
+            new Session(options) {
+              override val resources: Resources =
+                new Resources(session_background, log = log,
+                  command_timings =
+                    Properties.uncompress(
+                      session_context.old_command_timings_blob, cache = store.cache))
 
-          val session =
-            new Session(options, resources) {
               override val cache: Rich_Text.Cache = store.cache
 
               override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info =
@@ -321,7 +322,7 @@
           session.all_messages += Session.Consumer[Any]("build_session_output") {
             case msg: Prover.Output =>
               val message = msg.message
-              if (msg.is_system) resources.log(Protocol.message_text(message))
+              if (msg.is_system) session.resources.log(Protocol.message_text(message))
 
               if (msg.is_stdout) {
                 stdout ++= Symbol.encode(XML.content(message))
@@ -360,7 +361,7 @@
             Isabelle_Thread.interrupt_handler(_ => process.terminate()) {
               Exn.capture { process.await_startup() } match {
                 case Exn.Res(_) =>
-                  val resources_xml = resources.init_session_xml
+                  val resources_xml = session.resources.init_session_xml
                   val encode_options: XML.Encode.T[Options] =
                     options => session.prover_options(options).encode
                   val args_xml =
diff -r b00337cda5b9 -r 0ca8b1861fa3 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Jun 23 14:44:59 2025 +0200
+++ b/src/Pure/PIDE/headless.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -46,10 +46,11 @@
   class Session private[Headless](
     session_name: String,
     _session_options: => Options,
-    override val resources: Resources)
-  extends isabelle.Session(_session_options, resources) {
+    _resources: Headless.Resources)
+  extends isabelle.Session(_session_options) {
     session =>
 
+    override def resources: Headless.Resources = _resources
 
     private def loaded_theory(name: Document.Node.Name): Boolean =
       resources.session_base.loaded_theory(name.theory)
@@ -619,6 +620,7 @@
     ): Session = {
       val session_name = session_background.session_name
       val session = new Session(session_name, options, resources)
+
       val session_heaps = ML_Process.session_heaps(store, session_background, logic = session_name)
 
       progress.echo("Starting session " + session_name + " ...")
diff -r b00337cda5b9 -r 0ca8b1861fa3 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon Jun 23 14:44:59 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -121,9 +121,11 @@
 }
 
 
-class Session(_session_options: => Options, val resources: Resources) extends Document.Session {
+class Session(_session_options: => Options) extends Document.Session {
   session =>
 
+  def resources: Resources = Resources.bootstrap
+
   val init_time: Time = Time.now()
   def print_now(): String = (Time.now() - init_time).toString
 
diff -r b00337cda5b9 -r 0ca8b1861fa3 src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Mon Jun 23 14:44:59 2025 +0200
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -628,7 +628,7 @@
     val store = Store(options)
     val solr = Solr.init(solr_data_dir)
     val database = options.string("find_facts_database_name")
-    val session = Session(options, Resources.bootstrap)
+    val session = Session(options)
 
     val selection = Sessions.Selection(sessions = sessions)
     val sessions_structure =
diff -r b00337cda5b9 -r 0ca8b1861fa3 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Mon Jun 23 14:44:59 2025 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -114,9 +114,9 @@
 
   /* prover session */
 
-  private val session_ = Synchronized(None: Option[Session])
-  def session: Session = session_.value getOrElse error("Server inactive")
-  def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
+  private val session_ = Synchronized(None: Option[VSCode_Session])
+  def session: VSCode_Session = session_.value getOrElse error("Server inactive")
+  def resources: VSCode_Resources = session.resources
 
   def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     for {
@@ -285,7 +285,7 @@
           }
 
         val session_options = options.bool.update("editor_output_state", true)
-        val session = new Session(session_options, resources)
+        val session = new VSCode_Session(session_options, resources)
 
         Some((session_background, session))
       }
@@ -562,7 +562,7 @@
   object editor extends Language_Server.Editor {
     /* PIDE session and document model */
 
-    override def session: Session = server.session
+    override def session: VSCode_Session = server.session
     override def flush(): Unit = resources.flush_input(session, channel)
     override def invoke(): Unit = delay_input.invoke()
 
diff -r b00337cda5b9 -r 0ca8b1861fa3 src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Mon Jun 23 14:44:59 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_model.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -48,7 +48,7 @@
   }
 
   def init(
-    session: Session,
+    session: VSCode_Session,
     editor: Language_Server.Editor,
     node_name: Document.Node.Name
   ): VSCode_Model = {
@@ -59,7 +59,7 @@
 }
 
 sealed case class VSCode_Model(
-  session: Session,
+  session: VSCode_Session,
   editor: Language_Server.Editor,
   content: VSCode_Model.Content,
   version: Option[Long] = None,
@@ -92,8 +92,8 @@
   /* header */
 
   def node_header: Document.Node.Header =
-    resources.special_header(node_name) getOrElse
-      resources.check_thy(node_name, Scan.char_reader(content.text))
+    session.resources.special_header(node_name) getOrElse
+      session.resources.check_thy(node_name, Scan.char_reader(content.text))
 
 
   /* perspective */
@@ -103,11 +103,11 @@
     caret: Option[Line.Position]
   ): (Boolean, Document.Node.Perspective_Text.T) = {
     if (is_theory) {
-      val snapshot = resources.snapshot(model)
+      val snapshot = session.resources.snapshot(model)
 
       val required = node_required || editor.document_node_required(node_name)
 
-      val caret_perspective = resources.options.int("vscode_caret_perspective") max 0
+      val caret_perspective = session.resources.options.int("vscode_caret_perspective") max 0
       val caret_range =
         if (caret_perspective != 0) {
           caret match {
@@ -123,7 +123,7 @@
         else Text.Range.offside
 
       val text_perspective =
-        if (snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty)
+        if (snapshot.commands_loading_ranges(session.resources.visible_node(_)).nonEmpty)
           Text.Perspective.full
         else
           content.text_range.try_restrict(caret_range) match {
@@ -195,7 +195,7 @@
     rendering: VSCode_Rendering
   ): (Option[List[Text.Info[Command.Results]]], Option[List[VSCode_Model.Decoration]], VSCode_Model) = {
     val (diagnostics, decorations, model) = publish_full(rendering)
-    
+
     val changed_diagnostics =
       if (diagnostics == published_diagnostics) None else Some(diagnostics)
     val changed_decorations =
@@ -221,8 +221,6 @@
 
   /* prover session */
 
-  def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
-
   def is_stable: Boolean = pending_edits.isEmpty
 
 
diff -r b00337cda5b9 -r 0ca8b1861fa3 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Jun 23 14:44:59 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -67,10 +67,10 @@
 }
 
 class VSCode_Rendering(snapshot: Document.Snapshot, val model: VSCode_Model)
-extends Rendering(snapshot, model.resources.options, model.session) {
+extends Rendering(snapshot, model.session.resources.options, model.session) {
   rendering =>
 
-  def resources: VSCode_Resources = model.resources
+  def resources: VSCode_Resources = model.session.resources
 
   override def get_text(range: Text.Range): Option[String] = model.get_text(range)
 
@@ -264,7 +264,7 @@
     range: Symbol.Range
   ): Option[Line.Node_Range] = {
     for {
-      platform_path <- resources.source_file(model.resources.ml_settings, source_name)
+      platform_path <- resources.source_file(model.session.resources.ml_settings, source_name)
       file <-
         (try { Some(File.absolute(new JFile(platform_path))) }
          catch { case ERROR(_) => None })
diff -r b00337cda5b9 -r 0ca8b1861fa3 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Jun 23 14:44:59 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -185,7 +185,7 @@
     }
 
   def change_model(
-    session: Session,
+    session: VSCode_Session,
     editor: Language_Server.Editor,
     file: JFile,
     version: Long,
@@ -235,7 +235,7 @@
   /* resolve dependencies */
 
   def resolve_dependencies(
-    session: Session,
+    session: VSCode_Session,
     editor: Language_Server.Editor,
     file_watcher: File_Watcher
   ): (Boolean, Boolean) = {
@@ -270,7 +270,7 @@
 
   /* pending input */
 
-  def flush_input(session: Session, channel: Channel): Unit = {
+  def flush_input(session: VSCode_Session, channel: Channel): Unit = {
     state.change { st =>
       val changed_models =
         (for {
diff -r b00337cda5b9 -r 0ca8b1861fa3 src/Tools/VSCode/src/vscode_session.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/vscode_session.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -0,0 +1,18 @@
+/*  Title:      Tools/VSCode/src/vscode_session.scala
+    Author:     Makarius
+
+PIDE editor session for Isabelle/VSCode.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+
+class VSCode_Session(
+  _session_options: => Options,
+  _resources: VSCode_Resources
+) extends Session(_session_options) {
+  override def resources: VSCode_Resources = _resources
+}
diff -r b00337cda5b9 -r 0ca8b1861fa3 src/Tools/jEdit/src/jedit_session.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_session.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -0,0 +1,15 @@
+/*  Title:      Tools/jEdit/src/jedit_session.scala
+    Author:     Makarius
+
+PIDE editor session for Isabelle/jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+class JEdit_Session(_session_options: => Options) extends Session(_session_options) {
+  override val resources: JEdit_Resources = JEdit_Resources(_session_options)
+}
diff -r b00337cda5b9 -r 0ca8b1861fa3 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Mon Jun 23 14:44:59 2025 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -50,8 +50,8 @@
     else _plugin
 
   def options: JEdit_Options = plugin.options
-  def resources: JEdit_Resources = plugin.resources
-  def session: Session = plugin.session
+  def session: JEdit_Session = plugin.session
+  def resources: JEdit_Resources = session.resources
   def cache: Rich_Text.Cache = session.cache.asInstanceOf[Rich_Text.Cache]
 
   def ml_settings: ML_Settings = ML_Settings.system(plugin.startup_options)
@@ -77,18 +77,11 @@
   def options: JEdit_Options = _options
 
 
-  /* resources */
-
-  private var _resources: JEdit_Resources = null
-  private def init_resources(): Unit = _resources = JEdit_Resources(options.value)
-  def resources: JEdit_Resources = _resources
-
-
   /* session */
 
-  private var _session: Session = null
-  private def init_session(): Unit = { _session = new Session(options.value, resources) }
-  def session: Session = _session
+  private var _session: JEdit_Session = null
+  private def init_session(): Unit = { _session = new JEdit_Session(options.value) }
+  def session: JEdit_Session = _session
 
 
   /* misc support */
@@ -125,12 +118,12 @@
       val models = Document_Model.get_models_map()
 
       val thy_files =
-        resources.resolve_dependencies(models.values, PIDE.editor.document_required())
+        session.resources.resolve_dependencies(models.values, PIDE.editor.document_required())
 
       val aux_files =
-        if (resources.auto_resolve) {
+        if (session.resources.auto_resolve) {
           session.stable_tip_version(models.values) match {
-            case Some(version) => resources.undefined_blobs(version)
+            case Some(version) => session.resources.undefined_blobs(version)
             case None => delay_load.invoke(); Nil
           }
         }
@@ -144,7 +137,7 @@
           val loaded_files =
             for {
               name <- required_files
-              text <- resources.read_file_content(name)
+              text <- session.resources.read_file_content(name)
             } yield (name, text)
 
           GUI_Thread.later {
@@ -229,7 +222,7 @@
       } {
         if (buffer.isLoaded) {
           JEdit_Lib.buffer_lock(buffer) {
-            val node_name = resources.node_name(buffer)
+            val node_name = session.resources.node_name(buffer)
             val model = Document_Model.init(session, node_name, buffer)
             for {
               text_area <- JEdit_Lib.jedit_text_areas(buffer)
@@ -303,7 +296,7 @@
         case _: EditorStarted =>
           val view = jEdit.getActiveView
 
-          try { resources.session_background.check_errors }
+          try { session.resources.session_background.check_errors }
           catch {
             case ERROR(msg) =>
               GUI.warning_dialog(view,
@@ -429,7 +422,6 @@
     /* strict initialization */
 
     init_options()
-    init_resources()
     init_session()
     PIDE._plugin = this