--- a/src/Tools/jEdit/src/jedit_options.scala Sat Aug 13 23:08:07 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Sat Aug 13 23:47:08 2022 +0200
@@ -30,7 +30,7 @@
val RENDERING_SECTION = "Rendering of Document Content"
- /* typed access */
+ /* typed access and GUI components */
class Access[A](access: Options.Access_Variable[A], val name: String) {
def apply(): A = access.apply(name)
@@ -50,9 +50,6 @@
def toggle(): Unit = change(b => !b)
}
-
- /* GUI components */
-
class Bool_GUI(access: Bool_Access, label: String)
extends GUI.Check(label, init = access()) {
def load(): Unit = { selected = access() }