# 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