# HG changeset patch
# User wenzelm
# Date 1671451098 -3600
# Node ID ddf5764684dd2ccd86ca4fff16e68c023a5c3da3
# Parent  26f939b23fdd354172d1a45ac537a9e35b13ea88
proper state change, e.g. on open/close of "Document" panel;

diff -r 26f939b23fdd -r ddf5764684dd src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Dec 19 12:33:52 2022 +0100
+++ b/src/Pure/PIDE/editor.scala	Mon Dec 19 12:58:18 2022 +0100
@@ -22,10 +22,19 @@
 
   def document_session: Option[Sessions.Background] = document_editor.value.session_background
   def document_active: Boolean = document_editor.value.is_active
+  def document_active_changed(): Unit = {}
+  private def document_editor_change(f: Document_Editor.State => Document_Editor.State): Unit = {
+    val changed =
+      document_editor.change_result { st =>
+        val st1 = f(st)
+        (st.is_active != st1.is_active, st1)
+      }
+    if (changed) document_active_changed()
+  }
   def document_setup(background: Option[Sessions.Background]): Unit =
-    document_editor.change(_.copy(session_background = background))
-  def document_init(id: AnyRef): Unit = document_editor.change(_.register_view(id))
-  def document_exit(id: AnyRef): Unit = document_editor.change(_.unregister_view(id))
+    document_editor_change(_.copy(session_background = background))
+  def document_init(id: AnyRef): Unit = document_editor_change(_.register_view(id))
+  def document_exit(id: AnyRef): Unit = document_editor_change(_.unregister_view(id))
 
 
   /* current situation */
diff -r 26f939b23fdd -r ddf5764684dd src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 19 12:33:52 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 19 12:58:18 2022 +0100
@@ -53,6 +53,14 @@
     } yield doc_view.model.node_name).contains(name)
 
 
+  /* document editor */
+
+  override def document_active_changed(): Unit = {
+    PIDE.plugin.options_changed()
+    flush()
+  }
+
+
   /* current situation */
 
   override def current_node(view: View): Option[Document.Node.Name] =