# HG changeset patch
# User wenzelm
# Date 1660394736 -7200
# Node ID 7c00d5266bf8d64f90854d20da0452d8a112c844
# Parent  f8c412a45af8705950258dccaeec9e3fc0453f44
unused;

diff -r f8c412a45af8 -r 7c00d5266bf8 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Sat Aug 13 14:29:59 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Sat Aug 13 14:45:36 2022 +0200
@@ -27,23 +27,6 @@
 
 object JEdit_Options {
   val RENDERING_SECTION = "Rendering of Document Content"
-
-  class Check_Box(name: String, label: String, description: String) extends CheckBox(label) {
-    tooltip = description
-    reactions += { case ButtonClicked(_) => update(selected) }
-
-    def stored: Boolean = PIDE.options.bool(name)
-    def update(b: Boolean): Unit =
-      GUI_Thread.require {
-        if (selected != b) selected = b
-        if (stored != b) {
-          PIDE.options.bool(name) = b
-          PIDE.session.update_options(PIDE.options.value)
-        }
-      }
-    def load(): Unit = { selected = stored }
-    load()
-  }
 }
 
 class JEdit_Options(init_options: Options) extends Options_Variable(init_options) {