# HG changeset patch
# User wenzelm
# Date 1660419825 -7200
# Node ID 56f3032f0747d45ac737b87fd22d30bb96b75b22
# Parent  4cd3036e1b82bb325fc284e41ca3008c8c10d113
clarified signature;

diff -r 4cd3036e1b82 -r 56f3032f0747 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Sat Aug 13 21:42:52 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Sat Aug 13 21:43:45 2022 +0200
@@ -52,6 +52,18 @@
   }
 
 
+  /* GUI components */
+
+  class Bool_GUI(access: Bool_Access, label: String, description: String)
+  extends CheckBox(label) {
+    tooltip = description
+    reactions += { case ButtonClicked(_) => access.update(selected) }
+    def load(): Unit = { selected = access() }
+
+    load()
+  }
+
+
   /* specific options */
 
   object continuous_checking extends Bool_Access("editor_continuous_checking") {
@@ -60,12 +72,8 @@
       PIDE.plugin.deps_changed()
     }
 
-    class GUI extends CheckBox("Continuous checking") {
-      tooltip = "Continuous checking of proof document (visible and required parts)"
-      reactions += { case ButtonClicked(_) => continuous_checking.update(selected) }
-      def load(): Unit = { selected = continuous_checking() }
-      load()
-    }
+    class GUI extends Bool_GUI(this, "Continuous checking",
+      "Continuous checking of proof document (visible and required parts)")
   }
 
   object output_state extends Bool_Access("editor_output_state") {
@@ -75,12 +83,8 @@
       PIDE.editor.flush()
     }
 
-    class GUI extends CheckBox("Proof state") {
-      tooltip = "Output of proof state (normally shown on State panel)"
-      reactions += { case ButtonClicked(_) => output_state.update(selected) }
-      def load(): Unit = { selected = output_state() }
-      load()
-    }
+    class GUI extends Bool_GUI(this, "Proof state",
+      "Output of proof state (normally shown on State panel)")
   }
 }