--- a/src/Tools/jEdit/src/document_dockable.scala Sat Aug 13 22:41:45 2022 +0200
+++ b/src/Tools/jEdit/src/document_dockable.scala Sat Aug 13 23:04:53 2022 +0200
@@ -12,9 +12,6 @@
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}
-import scala.swing.Button
-import scala.swing.event.ButtonClicked
-
import org.gjt.sp.jedit.{jEdit, View}
@@ -56,9 +53,10 @@
val title = "Session"
}
- private val build_button = new Button("<html><b>Build</b></html>") {
+ private val build_button =
+ new GUI.Button("<html><b>Build</b></html>") {
tooltip = "Build document"
- reactions += { case ButtonClicked(_) =>
+ override def clicked(): Unit = {
pretty_text_area.update(
Document.Snapshot.init, Command.Results.empty,
List(XML.Text(Date.now().toString))) // FIXME