# HG changeset patch
# User wenzelm
# Date 1660424693 -7200
# Node ID f981111768ec395fa7e599f9d3d785c1134d7dec
# Parent fcc25bb49defad06d05bc34449bfc34cf577bdc7
clarified signature;
diff -r fcc25bb49def -r f981111768ec src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala Sat Aug 13 22:41:45 2022 +0200
+++ b/src/Pure/GUI/gui.scala Sat Aug 13 23:04:53 2022 +0200
@@ -113,6 +113,12 @@
/* basic GUI components */
+ class Button(label: String) extends scala.swing.Button(label) {
+ def clicked(): Unit = {}
+
+ reactions += { case ButtonClicked(_) => clicked() }
+ }
+
class Bool(label: String, init: Boolean = false) extends CheckBox(label) {
def clicked(state: Boolean): Unit = {}
def clicked(): Unit = {}
diff -r fcc25bb49def -r f981111768ec src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala Sat Aug 13 22:41:45 2022 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Sat Aug 13 23:04:53 2022 +0200
@@ -187,24 +187,24 @@
override def clicked(state: Boolean): Unit = debugger.set_break(state)
}
- private val continue_button = new Button("Continue") {
+ private val continue_button = new GUI.Button("Continue") {
tooltip = "Continue program on current thread, until next breakpoint"
- reactions += { case ButtonClicked(_) => thread_selection().map(debugger.continue) }
+ override def clicked(): Unit = thread_selection().map(debugger.continue)
}
- private val step_button = new Button("Step") {
+ private val step_button = new GUI.Button("Step") {
tooltip = "Single-step in depth-first order"
- reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step) }
+ override def clicked(): Unit = thread_selection().map(debugger.step)
}
- private val step_over_button = new Button("Step over") {
+ private val step_over_button = new GUI.Button("Step over") {
tooltip = "Single-step within this function"
- reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_over) }
+ override def clicked(): Unit = thread_selection().map(debugger.step_over)
}
- private val step_out_button = new Button("Step out") {
+ private val step_out_button = new GUI.Button("Step out") {
tooltip = "Single-step outside this function"
- reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_out) }
+ override def clicked(): Unit = thread_selection().map(debugger.step_out)
}
private val context_label = new Label("Context:") {
@@ -240,9 +240,10 @@
setFont(GUI.imitate_font(getFont, scale = 1.2))
}
- private val eval_button = new Button("Eval") {
+ private val eval_button =
+ new GUI.Button("Eval") {
tooltip = "Evaluate ML expression within optional context"
- reactions += { case ButtonClicked(_) => eval_expression() }
+ override def clicked(): Unit = eval_expression()
}
private def eval_expression(): Unit = {
diff -r fcc25bb49def -r f981111768ec src/Tools/jEdit/src/document_dockable.scala
--- 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("Build") {
+ private val build_button =
+ new GUI.Button("Build") {
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
diff -r fcc25bb49def -r f981111768ec src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala Sat Aug 13 22:41:45 2022 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Sat Aug 13 23:04:53 2022 +0200
@@ -12,8 +12,8 @@
import java.awt.BorderLayout
import scala.collection.immutable.Queue
-import scala.swing.{TextField, Button}
-import scala.swing.event.{ButtonClicked, ValueChanged}
+import scala.swing.TextField
+import scala.swing.event.ValueChanged
import org.jfree.chart.ChartPanel
import org.jfree.data.xy.XYSeriesCollection
@@ -78,25 +78,19 @@
reactions += { case ValueChanged(_) => input_delay.invoke() }
}
- private val reset_data = new Button("Reset") {
+ private val reset_data = new GUI.Button("Reset") {
tooltip = "Reset accumulated data"
- reactions += { case ButtonClicked(_) => clear_statistics(); update_chart() }
+ override def clicked(): Unit = { clear_statistics(); update_chart() }
}
- private val full_gc = new Button("GC") {
+ private val full_gc = new GUI.Button("GC") {
tooltip = "Full garbage collection of ML heap"
- reactions += {
- case ButtonClicked(_) =>
- PIDE.session.protocol_command("ML_Heap.full_gc")
- }
+ override def clicked(): Unit = PIDE.session.protocol_command("ML_Heap.full_gc")
}
- private val share_common_data = new Button("Sharing") {
+ private val share_common_data = new GUI.Button("Sharing") {
tooltip = "Share common data of ML heap"
- reactions += {
- case ButtonClicked(_) =>
- PIDE.session.protocol_command("ML_Heap.share_common_data")
- }
+ override def clicked(): Unit = PIDE.session.protocol_command("ML_Heap.share_common_data")
}
private val controls =
diff -r fcc25bb49def -r f981111768ec 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() }
diff -r fcc25bb49def -r f981111768ec src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala Sat Aug 13 22:41:45 2022 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Sat Aug 13 23:04:53 2022 +0200
@@ -12,8 +12,8 @@
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
import javax.swing.{JComponent, JTextField}
-import scala.swing.{Button, Component, TextField, Label, ListView, TabbedPane, BorderPanel}
-import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
+import scala.swing.{Component, TextField, Label, ListView, TabbedPane, BorderPanel}
+import scala.swing.event.{SelectionChanged, Key, KeyPressed}
import org.gjt.sp.jedit.View
@@ -110,9 +110,9 @@
override def clicked(): Unit = apply_query()
}
- private val apply_button = new Button("Apply") {
+ private val apply_button = new GUI.Button("Apply") {
tooltip = "Find theorems meeting specified criteria"
- reactions += { case ButtonClicked(_) => apply_query() }
+ override def clicked(): Unit = apply_query()
}
private val control_panel =
@@ -159,9 +159,9 @@
/* GUI page */
- private val apply_button = new Button("Apply") {
+ private val apply_button = new GUI.Button("Apply") {
tooltip = "Find constants by name / type patterns"
- reactions += { case ButtonClicked(_) => apply_query() }
+ override def clicked(): Unit = apply_query()
}
private val control_panel =
@@ -233,11 +233,12 @@
/* GUI page */
- private val apply_button = new Button("Apply") {
+ private val apply_button = new GUI.Button("Apply") {
tooltip = "Apply to current context"
+ override def clicked(): Unit = apply_query()
+
listenTo(keys)
reactions += {
- case ButtonClicked(_) => apply_query()
case evt @ KeyPressed(_, Key.Enter, 0, _) =>
evt.peer.consume()
apply_query()
diff -r fcc25bb49def -r f981111768ec src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala Sat Aug 13 22:41:45 2022 +0200
+++ b/src/Tools/jEdit/src/session_build.scala Sat Aug 13 23:04:53 2022 +0200
@@ -12,8 +12,7 @@
import java.awt.event.{WindowEvent, WindowAdapter}
import javax.swing.{WindowConstants, JDialog}
-import scala.swing.{ScrollPane, Button, FlowPanel, BorderPanel, TextArea, Component, Label}
-import scala.swing.event.ButtonClicked
+import scala.swing.{ScrollPane, FlowPanel, BorderPanel, TextArea, Component, Label}
import org.gjt.sp.jedit.View
@@ -96,7 +95,7 @@
Delay.first(Time.seconds(1.0), gui = true) {
if (can_auto_close) conclude()
else {
- val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } }
+ val button = new GUI.Button("Close") { override def clicked(): Unit = conclude() }
set_actions(button)
button.peer.getRootPane.setDefaultButton(button.peer)
}
@@ -124,8 +123,8 @@
set_actions(new Label("Stopping ..."))
}
- private val stop_button = new Button("Stop") {
- reactions += { case ButtonClicked(_) => stopping() }
+ private val stop_button = new GUI.Button("Stop") {
+ override def clicked(): Unit = stopping()
}
private var do_auto_close = true
diff -r fcc25bb49def -r f981111768ec src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- 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)
diff -r fcc25bb49def -r f981111768ec src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 13 22:41:45 2022 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 13 23:04:53 2022 +0200
@@ -9,8 +9,7 @@
import isabelle._
-import scala.swing.{Button, Component, Label}
-import scala.swing.event.ButtonClicked
+import scala.swing.{Component, Label}
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
@@ -68,7 +67,7 @@
/* controls */
- private def clicked(): Unit = {
+ private def hammer(): Unit = {
provers.addCurrentToHistory()
PIDE.options.string("sledgehammer_provers") = provers.getText
sledgehammer.apply_query(
@@ -84,7 +83,7 @@
private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
override def processKeyEvent(evt: KeyEvent): Unit = {
- if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked()
+ if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) hammer()
super.processKeyEvent(evt)
}
setToolTipText(provers_label.tooltip)
@@ -108,19 +107,19 @@
tooltip = "Try standard proof methods like \"auto\" and \"blast\" as alternatives to \"metis\""
}
- private val apply_query = new Button("Apply") {
+ private val apply_query = new GUI.Button("Apply") {
tooltip = "Search for first-order proof using automatic theorem provers"
- reactions += { case ButtonClicked(_) => clicked() }
+ override def clicked(): Unit = hammer()
}
- private val cancel_query = new Button("Cancel") {
+ private val cancel_query = new GUI.Button("Cancel") {
tooltip = "Interrupt unfinished sledgehammering"
- reactions += { case ButtonClicked(_) => sledgehammer.cancel_query() }
+ override def clicked(): Unit = sledgehammer.cancel_query()
}
- private val locate_query = new Button("Locate") {
+ private val locate_query = new GUI.Button("Locate") {
tooltip = "Locate context of current query within source text"
- reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
+ override def clicked(): Unit = sledgehammer.locate_query()
}
private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
diff -r fcc25bb49def -r f981111768ec src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala Sat Aug 13 22:41:45 2022 +0200
+++ b/src/Tools/jEdit/src/state_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}
@@ -86,14 +83,14 @@
}
}
- 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(_) => update_request() }
+ override def clicked(): Unit = update_request()
}
- private val locate_button = new Button("Locate") {
+ private val locate_button = new GUI.Button("Locate") {
tooltip = "Locate printed command within source text"
- reactions += { case ButtonClicked(_) => print_state.locate_query() }
+ override def clicked(): Unit = print_state.locate_query()
}
private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
diff -r fcc25bb49def -r f981111768ec src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 13 22:41:45 2022 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 13 23:04:53 2022 +0200
@@ -11,7 +11,7 @@
import scala.swing.{Button, TextArea, Label, ListView, Alignment,
ScrollPane, Component, CheckBox, BorderPanel}
-import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
+import scala.swing.event.{MouseClicked, MouseMoved}
import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
import javax.swing.{JList, BorderFactory, UIManager}
@@ -75,9 +75,9 @@
session_phase.text = " " + phase_text(phase) + " "
}
- private val purge = new Button("Purge") {
+ private val purge = new GUI.Button("Purge") {
tooltip = "Restrict document model to theories required for open editor buffers"
- reactions += { case ButtonClicked(_) => PIDE.editor.purge() }
+ override def clicked(): Unit = PIDE.editor.purge()
}
private val continuous_checking = new JEdit_Options.continuous_checking.GUI