# HG changeset patch
# User wenzelm
# Date 1660423305 -7200
# Node ID fcc25bb49defad06d05bc34449bfc34cf577bdc7
# Parent 56f3032f0747d45ac737b87fd22d30bb96b75b22
clarified signature;
diff -r 56f3032f0747 -r fcc25bb49def src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala Sat Aug 13 21:43:45 2022 +0200
+++ b/src/Pure/GUI/gui.scala Sat Aug 13 22:41:45 2022 +0200
@@ -13,8 +13,8 @@
import java.awt.geom.AffineTransform
import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities}
-import scala.swing.{ComboBox, ScrollPane, TextArea}
-import scala.swing.event.SelectionChanged
+import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea}
+import scala.swing.event.{ButtonClicked, SelectionChanged}
object GUI {
@@ -111,7 +111,15 @@
}
- /* variations on ComboBox */
+ /* basic GUI components */
+
+ class Bool(label: String, init: Boolean = false) extends CheckBox(label) {
+ def clicked(state: Boolean): Unit = {}
+ def clicked(): Unit = {}
+
+ selected = init
+ reactions += { case ButtonClicked(_) => clicked(selected); clicked() }
+ }
class Selector[A](val entries: List[A]) extends ComboBox[A](entries) {
def changed(): Unit = {}
@@ -120,6 +128,9 @@
reactions += { case SelectionChanged(_) => changed() }
}
+
+ /* zoom factor */
+
private val Zoom_Factor = "([0-9]+)%?".r
class Zoom extends Selector[String](
diff -r 56f3032f0747 -r fcc25bb49def src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala Sat Aug 13 21:43:45 2022 +0200
+++ b/src/Tools/Graphview/tree_panel.scala Sat Aug 13 22:41:45 2022 +0200
@@ -16,7 +16,7 @@
import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener, DocumentListener, DocumentEvent}
import scala.util.matching.Regex
-import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button, CheckBox, Action}
+import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button, Action}
class Tree_Panel(val graphview: Graphview, graph_panel: Graph_Panel)
diff -r 56f3032f0747 -r fcc25bb49def src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala Sat Aug 13 21:43:45 2022 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Sat Aug 13 22:41:45 2022 +0200
@@ -17,8 +17,7 @@
import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
import scala.collection.immutable.SortedMap
-import scala.swing.{Button, Label, Component, ScrollPane, SplitPane, Orientation,
- CheckBox, BorderPanel}
+import scala.swing.{Button, Label, Component, ScrollPane, SplitPane, Orientation, BorderPanel}
import scala.swing.event.ButtonClicked
import org.gjt.sp.jedit.{jEdit, View}
@@ -183,10 +182,9 @@
/* controls */
- private val break_button = new CheckBox("Break") {
+ private val break_button = new GUI.Bool("Break", init = debugger.is_break()) {
tooltip = "Break running threads at next possible breakpoint"
- selected = debugger.is_break()
- reactions += { case ButtonClicked(_) => debugger.set_break(selected) }
+ override def clicked(state: Boolean): Unit = debugger.set_break(state)
}
private val continue_button = new Button("Continue") {
@@ -257,9 +255,8 @@
}
}
- private val sml_button = new CheckBox("SML") {
+ private val sml_button = new GUI.Bool("SML") {
tooltip = "Official Standard ML instead of Isabelle/ML"
- selected = false
}
private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
diff -r 56f3032f0747 -r fcc25bb49def src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala Sat Aug 13 21:43:45 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Sat Aug 13 22:41:45 2022 +0200
@@ -11,8 +11,6 @@
import java.awt.{Point, Frame, Rectangle}
-import scala.swing.event.ButtonClicked
-
import org.gjt.sp.jedit.{jEdit, View, Buffer, EditBus}
import org.gjt.sp.jedit.msg.ViewUpdate
import org.gjt.sp.jedit.buffer.JEditBuffer
diff -r 56f3032f0747 -r fcc25bb49def src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala Sat Aug 13 21:43:45 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Sat Aug 13 22:41:45 2022 +0200
@@ -14,7 +14,6 @@
import javax.swing.text.JTextComponent
import scala.swing.{Component, CheckBox, TextArea}
-import scala.swing.event.ButtonClicked
import org.gjt.sp.jedit.gui.ColorWellButton
@@ -54,13 +53,10 @@
/* GUI components */
- class Bool_GUI(access: Bool_Access, label: String, description: String)
- extends CheckBox(label) {
- tooltip = description
- reactions += { case ButtonClicked(_) => access.update(selected) }
+ class Bool_GUI(access: Bool_Access, label: String)
+ extends GUI.Bool(label, init = access()) {
def load(): Unit = { selected = access() }
-
- load()
+ override def clicked(state: Boolean): Unit = access.update(state)
}
@@ -72,8 +68,9 @@
PIDE.plugin.deps_changed()
}
- class GUI extends Bool_GUI(this, "Continuous checking",
- "Continuous checking of proof document (visible and required parts)")
+ class GUI extends Bool_GUI(this, "Continuous checking") {
+ tooltip = "Continuous checking of proof document (visible and required parts)"
+ }
}
object output_state extends Bool_Access("editor_output_state") {
@@ -83,8 +80,9 @@
PIDE.editor.flush()
}
- class GUI extends Bool_GUI(this, "Proof state",
- "Output of proof state (normally shown on State panel)")
+ class GUI extends Bool_GUI(this, "Proof state") {
+ tooltip = "Output of proof state (normally shown on State panel)"
+ }
}
}
diff -r 56f3032f0747 -r fcc25bb49def src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala Sat Aug 13 21:43:45 2022 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Sat Aug 13 22:41:45 2022 +0200
@@ -9,7 +9,7 @@
import isabelle._
-import scala.swing.{Button, CheckBox}
+import scala.swing.Button
import scala.swing.event.ButtonClicked
import java.awt.BorderLayout
@@ -66,12 +66,12 @@
private val output_state_button = new JEdit_Options.output_state.GUI
- private val auto_update_button = new CheckBox("Auto update") {
+ private val auto_update_button = new GUI.Bool("Auto update", init = do_update) {
tooltip = "Indicate automatic update following cursor movement"
- reactions += {
- case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None)
+ override def clicked(state: Boolean): Unit = {
+ do_update = state
+ handle_update(do_update, None)
}
- selected = do_update
}
private val update_button = new Button("Update") {
diff -r 56f3032f0747 -r fcc25bb49def src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala Sat Aug 13 21:43:45 2022 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Sat Aug 13 22:41:45 2022 +0200
@@ -12,7 +12,7 @@
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
import javax.swing.{JComponent, JTextField}
-import scala.swing.{Button, Component, TextField, CheckBox, Label, ListView, TabbedPane, BorderPanel}
+import scala.swing.{Button, Component, TextField, Label, ListView, TabbedPane, BorderPanel}
import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
import org.gjt.sp.jedit.View
@@ -105,10 +105,9 @@
reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
}
- private val allow_dups = new CheckBox("Duplicates") {
+ private val allow_dups = new GUI.Bool("Duplicates") {
tooltip = "Show all versions of matching theorems"
- selected = false
- reactions += { case ButtonClicked(_) => apply_query() }
+ override def clicked(): Unit = apply_query()
}
private val apply_button = new Button("Apply") {
@@ -186,25 +185,24 @@
private val print_operation = new Query_Dockable.Operation(view) {
/* items */
- private class Item(val name: String, description: String, sel: Boolean) {
- val checkbox: CheckBox = new CheckBox(name) {
+ private class Item(val name: String, description: String, selected: Boolean) {
+ val gui: GUI.Bool = new GUI.Bool(name, init = selected) {
tooltip = "Print " + description
- selected = sel
- reactions += { case ButtonClicked(_) => apply_query() }
+ override def clicked(): Unit = apply_query()
}
}
private var _items: List[Item] = Nil
private def selected_items(): List[String] =
- for (item <- _items if item.checkbox.selected) yield item.name
+ for (item <- _items if item.gui.selected) yield item.name
private def update_items(): List[Item] = {
val old_items = _items
def was_selected(name: String): Boolean =
old_items.find(item => item.name == name) match {
case None => false
- case Some(item) => item.checkbox.selected
+ case Some(item) => item.gui.selected
}
_items =
@@ -251,7 +249,7 @@
def select(): Unit = {
control_panel.contents.clear()
control_panel.contents += query_label
- update_items().foreach(item => control_panel.contents += item.checkbox)
+ update_items().foreach(item => control_panel.contents += item.gui)
control_panel.contents ++=
List(process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_field, zoom)
diff -r 56f3032f0747 -r fcc25bb49def src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala Sat Aug 13 21:43:45 2022 +0200
+++ b/src/Tools/jEdit/src/session_build.scala Sat Aug 13 22:41:45 2022 +0200
@@ -12,8 +12,7 @@
import java.awt.event.{WindowEvent, WindowAdapter}
import javax.swing.{WindowConstants, JDialog}
-import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
- BorderPanel, TextArea, Component, Label}
+import scala.swing.{ScrollPane, Button, FlowPanel, BorderPanel, TextArea, Component, Label}
import scala.swing.event.ButtonClicked
import org.gjt.sp.jedit.View
@@ -132,14 +131,13 @@
private var do_auto_close = true
private def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
- private val auto_close = new CheckBox("Auto close") {
- reactions += {
- case ButtonClicked(_) => do_auto_close = this.selected
+ private val auto_close = new GUI.Bool("Auto close", init = do_auto_close) {
+ tooltip = "Automatically close dialog when finished"
+ override def clicked(state: Boolean): Unit = {
+ do_auto_close = state
if (can_auto_close) conclude()
}
}
- auto_close.selected = do_auto_close
- auto_close.tooltip = "Automatically close dialog when finished"
set_actions(stop_button, auto_close)
diff -r 56f3032f0747 -r fcc25bb49def src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Sat Aug 13 21:43:45 2022 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Sat Aug 13 22:41:45 2022 +0200
@@ -9,7 +9,7 @@
import isabelle._
-import scala.swing.{Button, CheckBox, Orientation, Separator}
+import scala.swing.{Button, Orientation, Separator}
import scala.swing.event.ButtonClicked
import java.awt.BorderLayout
@@ -146,10 +146,10 @@
private val controls =
Wrap_Panel(
List(
- new CheckBox("Auto update") {
- selected = do_update
- reactions += {
- case ButtonClicked(_) => do_update = this.selected; handle_update(do_update)
+ new GUI.Bool("Auto update", init = do_update) {
+ override def clicked(state: Boolean): Unit = {
+ do_update = state
+ handle_update(do_update)
}
},
new Button("Update") {
diff -r 56f3032f0747 -r fcc25bb49def src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Sat Aug 13 21:43:45 2022 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Sat Aug 13 22:41:45 2022 +0200
@@ -11,7 +11,7 @@
import scala.annotation.tailrec
import scala.collection.immutable.SortedMap
-import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
+import scala.swing.{BorderPanel, Component, Dimension, Frame, Label, TextField}
import scala.swing.event.{Key, KeyPressed}
import scala.util.matching.Regex
diff -r 56f3032f0747 -r fcc25bb49def src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 13 21:43:45 2022 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 13 22:41:45 2022 +0200
@@ -9,7 +9,7 @@
import isabelle._
-import scala.swing.{Button, Component, Label, CheckBox}
+import scala.swing.{Button, Component, Label}
import scala.swing.event.ButtonClicked
import java.awt.BorderLayout
@@ -100,14 +100,12 @@
}
}
- private val isar_proofs = new CheckBox("Isar proofs") {
+ private val isar_proofs = new GUI.Bool("Isar proofs") {
tooltip = "Specify whether Isar proofs should be output in addition to \"by\" one-liner"
- selected = false
}
- private val try0 = new CheckBox("Try methods") {
+ private val try0 = new GUI.Bool("Try methods", init = true) {
tooltip = "Try standard proof methods like \"auto\" and \"blast\" as alternatives to \"metis\""
- selected = true
}
private val apply_query = new Button("Apply") {
diff -r 56f3032f0747 -r fcc25bb49def src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala Sat Aug 13 21:43:45 2022 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala Sat Aug 13 22:41:45 2022 +0200
@@ -9,7 +9,7 @@
import isabelle._
-import scala.swing.{Button, CheckBox}
+import scala.swing.Button
import scala.swing.event.ButtonClicked
import java.awt.BorderLayout
@@ -78,10 +78,12 @@
/* controls */
- private val auto_update_button = new CheckBox("Auto update") {
+ private val auto_update_button = new GUI.Bool("Auto update", init = auto_update_enabled) {
tooltip = "Indicate automatic update following cursor movement"
- reactions += { case ButtonClicked(_) => auto_update_enabled = this.selected; auto_update() }
- selected = auto_update_enabled
+ override def clicked(state: Boolean): Unit = {
+ auto_update_enabled = state
+ auto_update()
+ }
}
private val update_button = new Button("Update") {