# HG changeset patch
# User wenzelm
# Date 1751024256 -7200
# Node ID 803731b62180ceed1e56c66b0346117aa71b14f6
# Parent  86a9aaa92877292cbbf7c0bd92c51c306add999b
clarified signature;
clarified modules;

diff -r 86a9aaa92877 -r 803731b62180 src/Pure/Build/resources.scala
--- a/src/Pure/Build/resources.scala	Fri Jun 27 13:24:05 2025 +0200
+++ b/src/Pure/Build/resources.scala	Fri Jun 27 13:37:36 2025 +0200
@@ -252,8 +252,6 @@
       consolidate: List[Document.Node.Name]): Session.Change =
     Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
 
-  def commit(change: Session.Change): Unit = {}
-
 
   /* theory and file dependencies */
 
diff -r 86a9aaa92877 -r 803731b62180 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Jun 27 13:24:05 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Jun 27 13:37:36 2025 +0200
@@ -273,6 +273,14 @@
       true
   }
 
+  def auto_resolve: Boolean = true
+  def deps_changed(): Unit = {}
+
+  def commit_change(change: Session.Change): Unit =
+    if (change.deps_changed || auto_resolve && resources.undefined_blobs(change.version).nonEmpty) {
+      deps_changed()
+    }
+
 
   /* buffered changes */
 
@@ -462,7 +470,7 @@
       global_state.change(_.define_version(change.version, assignment))
 
       prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate)
-      resources.commit(change)
+      commit_change(change)
     //}}}
     }
 
diff -r 86a9aaa92877 -r 803731b62180 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Fri Jun 27 13:24:05 2025 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Fri Jun 27 13:37:36 2025 +0200
@@ -274,15 +274,12 @@
           if (!build().ok) { progress.echo(fail_msg); error(fail_msg) }
         }
 
-        val session_resources =
-          new VSCode_Resources(options, session_background, log) {
-            override def commit(change: Session.Change): Unit =
-              if (change.deps_changed || undefined_blobs(change.version).nonEmpty) {
-                delay_load.invoke()
-              }
+        val session_resources = new VSCode_Resources(options, session_background, log)
+        val session_options = options.bool.update("editor_output_state", true)
+        val session =
+          new VSCode_Session(session_options, session_resources) {
+            override def deps_changed(): Unit = delay_load.invoke()
           }
-        val session_options = options.bool.update("editor_output_state", true)
-        val session = new VSCode_Session(session_options, session_resources)
 
         Some((session_background, session))
       }
diff -r 86a9aaa92877 -r 803731b62180 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Jun 27 13:24:05 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Jun 27 13:37:36 2025 +0200
@@ -60,7 +60,7 @@
 
   def state_changed(): Unit = {
     GUI_Thread.later { flush() }
-    PIDE.plugin.deps_changed()
+    PIDE.session.deps_changed()
     session.global_options.post(Session.Global_Options(PIDE.options.value))
   }
 
diff -r 86a9aaa92877 -r 803731b62180 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Fri Jun 27 13:24:05 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Fri Jun 27 13:37:36 2025 +0200
@@ -53,7 +53,7 @@
   object continuous_checking extends Bool_Access("editor_continuous_checking") {
     override def changed(): Unit = {
       super.changed()
-      PIDE.plugin.deps_changed()
+      PIDE.session.deps_changed()
     }
 
     class GUI extends Bool_GUI(this, "Continuous checking") {
diff -r 86a9aaa92877 -r 803731b62180 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Fri Jun 27 13:24:05 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri Jun 27 13:37:36 2025 +0200
@@ -129,18 +129,4 @@
   }
 
   def make_file_content(buffer: Buffer): Bytes = (new File_Content_Request(buffer)).content()
-
-
-  /* theory text edits */
-
-  def auto_resolve: Boolean = PIDE.options.bool("jedit_auto_resolve")
-
-  override def commit(change: Session.Change): Unit = {
-    if (change.syntax_changed.nonEmpty) {
-      GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) }
-    }
-    if (change.deps_changed || auto_resolve && undefined_blobs(change.version).nonEmpty) {
-      PIDE.plugin.deps_changed()
-    }
-  }
 }
diff -r 86a9aaa92877 -r 803731b62180 src/Tools/jEdit/src/jedit_session.scala
--- a/src/Tools/jEdit/src/jedit_session.scala	Fri Jun 27 13:24:05 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_session.scala	Fri Jun 27 13:37:36 2025 +0200
@@ -164,4 +164,6 @@
 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))
+
+  override def auto_resolve: Boolean = session_options.bool("jedit_auto_resolve")
 }
diff -r 86a9aaa92877 -r 803731b62180 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Fri Jun 27 13:24:05 2025 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Fri Jun 27 13:37:36 2025 +0200
@@ -78,7 +78,12 @@
   /* session */
 
   private var _session: JEdit_Session = null
-  private def init_session(): Unit = { _session = new JEdit_Session(options.value) }
+  private def init_session(): Unit = {
+    _session =
+      new JEdit_Session(options.value) {
+        override def deps_changed(): Unit = delay_load.invoke()
+      }
+  }
   def session: JEdit_Session = _session
 
 
@@ -104,8 +109,6 @@
       }
     }
 
-  def deps_changed(): Unit = delay_load.invoke()
-
   private val delay_load_active = Synchronized(false)
   private def delay_load_finished(): Unit = delay_load_active.change(_ => false)
   private def delay_load_activated(): Boolean =
@@ -119,7 +122,7 @@
         session.resources.resolve_dependencies(models.values, PIDE.editor.document_required())
 
       val aux_files =
-        if (session.resources.auto_resolve) {
+        if (session.auto_resolve) {
           session.stable_tip_version(models.values) match {
             case Some(version) => session.resources.undefined_blobs(version)
             case None => delay_load.invoke(); Nil