# HG changeset patch
# User wenzelm
# Date 1675184607 -3600
# Node ID e3a7d36686294fe944081b9104afcbc52557e8ad
# Parent  6840013a791aef9e901f587eaed7f725421db172
clarified GUI events: ensure fresh output when switching pages;

diff -r 6840013a791a -r e3a7d3668629 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:46:16 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 18:03:27 2023 +0100
@@ -76,6 +76,7 @@
   }
 
   private def show_page(page: TabbedPane.Page): Unit = GUI_Thread.later {
+    show_state()
     message_pane.selection.page = page
   }
 
@@ -108,7 +109,7 @@
       Delay.first(PIDE.session.output_delay) {
         if (!stopped) {
           output_process(progress)
-          GUI_Thread.later { show_state() }
+          show_state()
         }
       }
 
@@ -186,17 +187,13 @@
         finish_process(Nil)
         GUI_Thread.later {
           refresh_theories()
-          show_state()
           show_page(input_page)
         }
       }
       catch {
         case exn: Throwable if !Exn.is_interrupt(exn) =>
           finish_process(List(Protocol.error_message(Exn.print(exn))))
-          GUI_Thread.later {
-            show_state()
-            show_page(output_page)
-          }
+          show_page(output_page)
       }
     }
   }
@@ -250,7 +247,6 @@
         progress.stop()
         finish_process(Pretty.separate(msgs))
 
-        show_state()
         show_page(output_page)
       }
       true