# HG changeset patch
# User wenzelm
# Date 1666967144 -7200
# Node ID 3fa81de0b6c55fd94f64d6aeb569fb78c882adad
# Parent  6129e8cb140db11aa1d4bc87668aa8668ef0d35b
tuned;

diff -r 6129e8cb140d -r 3fa81de0b6c5 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Fri Oct 28 16:14:14 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Fri Oct 28 16:25:44 2022 +0200
@@ -20,11 +20,6 @@
 
 
 object JEdit_Options {
-  /* sections */
-
-  val RENDERING_SECTION = "Rendering of Document Content"
-
-
   /* typed access and GUI components */
 
   class Access[A](access: Options.Access_Variable[A], val name: String) {
@@ -107,7 +102,6 @@
     }
   }
 
-
   class Isabelle_General_Options extends Isabelle_Options("isabelle-general") {
     val options: JEdit_Options = PIDE.options
 
@@ -120,12 +114,11 @@
         (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet)
   }
 
-
   class Isabelle_Rendering_Options extends Isabelle_Options("isabelle-rendering") {
     private val predefined =
       (for {
         (name, opt) <- PIDE.options.value.opt_iterator
-        if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
+        if name.endsWith("_color") && opt.section == "Rendering of Document Content"
       } yield PIDE.options.make_color_component(opt)).toList
 
     assert(predefined.nonEmpty)