# HG changeset patch # User wenzelm # Date 1675262388 -3600 # Node ID 2ddb82044ff055fe12126e10e464fd6a4db2a104 # Parent b2bc810e4bf70feb871e52bf0d558071666e403f clarified GUI; diff -r b2bc810e4bf7 -r 2ddb82044ff0 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Wed Feb 01 13:50:53 2023 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Wed Feb 01 15:39:48 2023 +0100 @@ -313,12 +313,6 @@ override def clicked(): Unit = pending_process() } - private val cancel_button = - new GUI.Button("Cancel") { - tooltip = "Cancel build process" - override def clicked(): Unit = cancel_process() - } - private val view_button = new GUI.Button("View") { tooltip = "View document" @@ -327,7 +321,7 @@ private val controls = Wrap_Panel(List(document_session, process_indicator.component, - auto_build_button, build_button, view_button, cancel_button)) + auto_build_button, build_button, view_button)) add(controls.peer, BorderLayout.NORTH) @@ -371,7 +365,14 @@ layout(theories_pane) = BorderPanel.Position.Center }, "Selection and status of document theories") - private val output_controls = Wrap_Panel(List(zoom)) + + private val cancel_button = + new GUI.Button("Cancel") { + tooltip = "Cancel build process" + override def clicked(): Unit = cancel_process() + } + + private val output_controls = Wrap_Panel(List(cancel_button, zoom)) private val output_page = new TabbedPane.Page("Output", new BorderPanel {