clarified GUI;
authorwenzelm
Wed, 01 Feb 2023 15:39:48 +0100
changeset 77170 2ddb82044ff0
parent 77169 b2bc810e4bf7
child 77171 e0e9f1b4c844
clarified GUI;
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 {