# HG changeset patch
# User wenzelm
# Date 1671618624 -3600
# Node ID c8d5cc19270a3d535054d94e28c184bba4746697
# Parent  6969d0ffc576cf5edbb819c46fa3ead6e4881830
more thorough GUI updates, notably for multiple Document dockables;

diff -r 6969d0ffc576 -r c8d5cc19270a src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Tue Dec 20 22:24:36 2022 +0000
+++ b/src/Pure/PIDE/editor.scala	Wed Dec 21 11:30:24 2022 +0100
@@ -27,7 +27,10 @@
     val changed =
       document_editor.change_result { st =>
         val st1 = f(st)
-        (st.required != st1.required, st1)
+        val changed =
+          st.active_document_theories != st1.active_document_theories ||
+          st.required != st1.required
+        (changed, st1)
       }
     if (changed) document_state_changed()
   }
diff -r 6969d0ffc576 -r c8d5cc19270a src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Dec 20 22:24:36 2022 +0000
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Dec 21 11:30:24 2022 +0100
@@ -160,8 +160,7 @@
 
         finish_process(Nil)
         GUI_Thread.later {
-          val domain = PIDE.editor.document_theories().toSet
-          theories.update(domain = Some(domain), trim = true, force = true)
+          refresh_theories()
           show_state()
           show_page(theories_page)
         }
@@ -267,6 +266,12 @@
 
   private val theories = new Theories_Status(view, document = true)
 
+  private def refresh_theories(): Unit = {
+    val domain = PIDE.editor.document_theories().toSet
+    theories.update(domain = Some(domain), trim = true, force = true)
+    theories.refresh()
+  }
+
   private val theories_page =
     new TabbedPane.Page("Theories", new BorderPanel {
       layout(theories_controls) = BorderPanel.Position.North
@@ -300,7 +305,7 @@
         GUI_Thread.later {
           document_session.load()
           handle_resize()
-          theories.refresh()
+          refresh_theories()
         }
       case changed: Session.Commands_Changed =>
         GUI_Thread.later {