# HG changeset patch
# User wenzelm
# Date 1660424887 -7200
# Node ID 2163772eeaf283da3a12dc2809bbd013ce4f3f8f
# Parent  f981111768ec395fa7e599f9d3d785c1134d7dec
tuned signature;

diff -r f981111768ec -r 2163772eeaf2 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Sat Aug 13 23:04:53 2022 +0200
+++ b/src/Pure/GUI/gui.scala	Sat Aug 13 23:08:07 2022 +0200
@@ -119,7 +119,7 @@
     reactions += { case ButtonClicked(_) => clicked() }
   }
 
-  class Bool(label: String, init: Boolean = false) extends CheckBox(label) {
+  class Check(label: String, init: Boolean = false) extends CheckBox(label) {
     def clicked(state: Boolean): Unit = {}
     def clicked(): Unit = {}
 
diff -r f981111768ec -r 2163772eeaf2 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sat Aug 13 23:04:53 2022 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sat Aug 13 23:08:07 2022 +0200
@@ -182,7 +182,7 @@
 
   /* controls */
 
-  private val break_button = new GUI.Bool("Break", init = debugger.is_break()) {
+  private val break_button = new GUI.Check("Break", init = debugger.is_break()) {
     tooltip = "Break running threads at next possible breakpoint"
     override def clicked(state: Boolean): Unit = debugger.set_break(state)
   }
@@ -256,7 +256,7 @@
     }
   }
 
-  private val sml_button = new GUI.Bool("SML") {
+  private val sml_button = new GUI.Check("SML") {
     tooltip = "Official Standard ML instead of Isabelle/ML"
   }
 
diff -r f981111768ec -r 2163772eeaf2 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Sat Aug 13 23:04:53 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Sat Aug 13 23:08:07 2022 +0200
@@ -54,7 +54,7 @@
   /* GUI components */
 
   class Bool_GUI(access: Bool_Access, label: String)
-  extends GUI.Bool(label, init = access()) {
+  extends GUI.Check(label, init = access()) {
     def load(): Unit = { selected = access() }
     override def clicked(state: Boolean): Unit = access.update(state)
   }
diff -r f981111768ec -r 2163772eeaf2 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sat Aug 13 23:04:53 2022 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Aug 13 23:08:07 2022 +0200
@@ -63,7 +63,7 @@
 
   private val output_state_button = new JEdit_Options.output_state.GUI
 
-  private val auto_update_button = new GUI.Bool("Auto update", init = do_update) {
+  private val auto_update_button = new GUI.Check("Auto update", init = do_update) {
     tooltip = "Indicate automatic update following cursor movement"
     override def clicked(state: Boolean): Unit = {
       do_update = state
diff -r f981111768ec -r 2163772eeaf2 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Sat Aug 13 23:04:53 2022 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Sat Aug 13 23:08:07 2022 +0200
@@ -105,7 +105,7 @@
       reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
     }
 
-    private val allow_dups = new GUI.Bool("Duplicates") {
+    private val allow_dups = new GUI.Check("Duplicates") {
       tooltip = "Show all versions of matching theorems"
       override def clicked(): Unit = apply_query()
     }
@@ -186,7 +186,7 @@
     /* items */
 
     private class Item(val name: String, description: String, selected: Boolean) {
-      val gui: GUI.Bool = new GUI.Bool(name, init = selected) {
+      val gui: GUI.Check = new GUI.Check(name, init = selected) {
         tooltip = "Print " + description
         override def clicked(): Unit = apply_query()
       }
diff -r f981111768ec -r 2163772eeaf2 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Sat Aug 13 23:04:53 2022 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Sat Aug 13 23:08:07 2022 +0200
@@ -130,7 +130,7 @@
     private var do_auto_close = true
     private def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
 
-    private val auto_close = new GUI.Bool("Auto close", init = do_auto_close) {
+    private val auto_close = new GUI.Check("Auto close", init = do_auto_close) {
       tooltip = "Automatically close dialog when finished"
       override def clicked(state: Boolean): Unit = {
         do_auto_close = state
diff -r f981111768ec -r 2163772eeaf2 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Sat Aug 13 23:04:53 2022 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Sat Aug 13 23:08:07 2022 +0200
@@ -143,7 +143,7 @@
   private val controls =
     Wrap_Panel(
       List(
-        new GUI.Bool("Auto update", init = do_update) {
+        new GUI.Check("Auto update", init = do_update) {
           override def clicked(state: Boolean): Unit = {
             do_update = state
             handle_update(do_update)
diff -r f981111768ec -r 2163772eeaf2 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Aug 13 23:04:53 2022 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Aug 13 23:08:07 2022 +0200
@@ -99,11 +99,11 @@
     }
   }
 
-  private val isar_proofs = new GUI.Bool("Isar proofs") {
+  private val isar_proofs = new GUI.Check("Isar proofs") {
     tooltip = "Specify whether Isar proofs should be output in addition to \"by\" one-liner"
   }
 
-  private val try0 = new GUI.Bool("Try methods", init = true) {
+  private val try0 = new GUI.Check("Try methods", init = true) {
     tooltip = "Try standard proof methods like \"auto\" and \"blast\" as alternatives to \"metis\""
   }
 
diff -r f981111768ec -r 2163772eeaf2 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Sat Aug 13 23:04:53 2022 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala	Sat Aug 13 23:08:07 2022 +0200
@@ -75,7 +75,7 @@
 
   /* controls */
 
-  private val auto_update_button = new GUI.Bool("Auto update", init = auto_update_enabled) {
+  private val auto_update_button = new GUI.Check("Auto update", init = auto_update_enabled) {
     tooltip = "Indicate automatic update following cursor movement"
     override def clicked(state: Boolean): Unit = {
       auto_update_enabled = state