# HG changeset patch # User wenzelm # Date 1662022350 -7200 # Node ID dda3c117f13ced4dfaa9f2c7578135845d049d46 # Parent 97b6daab02335cf1557c2d6581ef673133062b60 clarified GUI behaviour; diff -r 97b6daab0233 -r dda3c117f13c src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Wed Aug 31 23:05:12 2022 +0200 +++ b/src/Tools/jEdit/src/document_dockable.scala Thu Sep 01 10:52:30 2022 +0200 @@ -56,7 +56,7 @@ private val pretty_text_area = new Pretty_Text_Area(view) private val message_pane = new TabbedPane - private def show_state(show_output: Boolean = false): Unit = GUI_Thread.later { + private def show_state(): Unit = GUI_Thread.later { val st = current_state.value pretty_text_area.update(Document.Snapshot.init, Command.Results.empty, st.output) @@ -69,8 +69,10 @@ case Document_Dockable.Status.FINISHED => process_indicator.update(null, 0) } + } - if (show_output && output_page != null) message_pane.selection.page = output_page + private def show_page(page: TabbedPane.Page): Unit = GUI_Thread.later { + message_pane.selection.page = page } @@ -123,7 +125,8 @@ private def finish(result: Document_Dockable.Result): Unit = { current_state.change { _ => Document_Dockable.State.finish(result) } - show_state(show_output = result.failed) + show_state() + show_page(output_page) } private def build_document(): Unit = { @@ -132,6 +135,7 @@ val progress = init_progress() val process = Future.thread[Unit](name = "document_build") { + show_page(log_page) val res = Exn.capture { progress.echo("Start " + Date.now())