src/Tools/jEdit/src/simplifier_trace_dockable.scala
changeset 75853 f981111768ec
parent 75852 fcc25bb49def
child 75854 2163772eeaf2
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Sat Aug 13 22:41:45 2022 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Sat Aug 13 23:04:53 2022 +0200
@@ -9,8 +9,7 @@
 
 import isabelle._
 
-import scala.swing.{Button, Orientation, Separator}
-import scala.swing.event.ButtonClicked
+import scala.swing.{Orientation, Separator}
 
 import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter}
@@ -45,11 +44,9 @@
         val content = Pretty.separate(XML.Text(data.text) :: data.content)
         text_area.update(snapshot, Command.Results.empty, content)
         q.answers.foreach { answer =>
-          answers.contents += new Button(answer.string) {
-            reactions += {
-              case ButtonClicked(_) =>
-                Simplifier_Trace.send_reply(PIDE.session, data.serial, answer)
-            }
+          answers.contents += new GUI.Button(answer.string) {
+            override def clicked(): Unit =
+              Simplifier_Trace.send_reply(PIDE.session, data.serial, answer)
           }
         }
       case Nil =>
@@ -152,17 +149,11 @@
             handle_update(do_update)
           }
         },
-        new Button("Update") {
-          reactions += { case ButtonClicked(_) => handle_update(true) }
-        },
+        new GUI.Button("Update") { override def clicked(): Unit = handle_update(true) },
         new Separator(Orientation.Vertical),
-        new Button("Show trace") {
-          reactions += { case ButtonClicked(_) => show_trace() }
-        },
-        new Button("Clear memory") {
-          reactions += {
-            case ButtonClicked(_) => Simplifier_Trace.clear_memory(PIDE.session)
-          }
+        new GUI.Button("Show trace") { override def clicked(): Unit = show_trace() },
+        new GUI.Button("Clear memory") {
+          override def clicked(): Unit = Simplifier_Trace.clear_memory(PIDE.session)
         }))
 
   private val answers = Wrap_Panel(Nil, Wrap_Panel.Alignment.Left)