# HG changeset patch
# User wenzelm
# Date 1671451619 -3600
# Node ID 3d4358e016467f828d74b55b0a64714d2dfe5d85
# Parent  ddf5764684dd2ccd86ca4fff16e68c023a5c3da3
clarified state change: presumably more robust;

diff -r ddf5764684dd -r 3d4358e01646 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Dec 19 12:58:18 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Dec 19 13:06:59 2022 +0100
@@ -211,10 +211,7 @@
               case _ => (false, st)
             }
         })
-    if (changed) {
-      PIDE.plugin.options_changed()
-      PIDE.editor.flush()
-    }
+    if (changed) PIDE.editor.state_changed()
   }
 
   def view_node_required(
diff -r ddf5764684dd -r 3d4358e01646 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 19 12:58:18 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 19 13:06:59 2022 +0100
@@ -53,13 +53,16 @@
     } yield doc_view.model.node_name).contains(name)
 
 
-  /* document editor */
+  /* global changes */
 
-  override def document_active_changed(): Unit = {
-    PIDE.plugin.options_changed()
+  def state_changed(): Unit = {
     flush()
+    PIDE.plugin.deps_changed()
+    session.global_options.post(Session.Global_Options(PIDE.options.value))
   }
 
+  override def document_active_changed(): Unit = state_changed()
+
 
   /* current situation */
 
diff -r ddf5764684dd -r 3d4358e01646 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Mon Dec 19 12:58:18 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Mon Dec 19 13:06:59 2022 +0100
@@ -101,6 +101,8 @@
       }
     }
 
+  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 =
@@ -153,18 +155,6 @@
     File_Watcher(file_watcher_action, session.load_delay)
 
 
-  /* global changes */
-
-  def options_changed(): Unit = {
-    session.global_options.post(Session.Global_Options(options.value))
-    delay_load.invoke()
-  }
-
-  def deps_changed(): Unit = {
-    delay_load.invoke()
-  }
-
-
   /* session phase */
 
   val session_phase_changed: Session.Consumer[Session.Phase] = Session.Consumer("Isabelle/jEdit") {