src/Tools/jEdit/src/output_dockable.scala

--- a/src/Tools/jEdit/src/output_dockable.scala	Sat Aug 13 22:41:45 2022 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Aug 13 23:04:53 2022 +0200
@@ -9,9 +9,6 @@
 
 import isabelle._
 
-import scala.swing.Button
-import scala.swing.event.ButtonClicked
-
 import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter}
 
@@ -74,9 +71,9 @@
     }
   }
 
-  private val update_button = new Button("Update") {
+  private val update_button = new GUI.Button("Update") {
     tooltip = "Update display according to the command at cursor position"
-    reactions += { case ButtonClicked(_) => handle_update(true, None) }
+    override def clicked(): Unit = handle_update(true, None)
   }
 
   private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }