# HG changeset patch
# User wenzelm
# Date 1660427228 -7200
# Node ID 9ce4cb8e3f77a44c63a0a74f2a94861a72401869
# Parent  2163772eeaf283da3a12dc2809bbd013ce4f3f8f
tuned comments;

diff -r 2163772eeaf2 -r 9ce4cb8e3f77 src/Tools/jEdit/src/jedit_options.scala
--- 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() }