diff --git a/etc/build.props b/etc/build.props
--- a/etc/build.props
+++ b/etc/build.props
@@ -1,313 +1,312 @@
 title = Isabelle/Scala
 module = $ISABELLE_HOME/lib/classes/isabelle.jar
 main = isabelle.jedit.JEdit_Main
 resources = \
   lib/services/java.nio.charset.spi.CharsetProvider:META-INF/services/ \
   lib/logo/isabelle_transparent-32.gif:isabelle/ \
   lib/logo/isabelle_transparent.gif:isabelle/
 sources = \
   src/HOL/SPARK/Tools/spark.scala \
   src/HOL/Tools/ATP/system_on_tptp.scala \
   src/HOL/Tools/Mirabelle/mirabelle.scala \
   src/HOL/Tools/Nitpick/kodkod.scala \
   src/Pure/Admin/afp.scala \
   src/Pure/Admin/build_cvc5.scala \
   src/Pure/Admin/build_csdp.scala \
   src/Pure/Admin/build_cygwin.scala \
   src/Pure/Admin/build_doc.scala \
   src/Pure/Admin/build_e.scala \
   src/Pure/Admin/build_fonts.scala \
   src/Pure/Admin/build_history.scala \
   src/Pure/Admin/build_jcef.scala \
   src/Pure/Admin/build_jdk.scala \
   src/Pure/Admin/build_jedit.scala \
   src/Pure/Admin/build_log.scala \
   src/Pure/Admin/build_minisat.scala \
   src/Pure/Admin/build_pdfjs.scala \
   src/Pure/Admin/build_polyml.scala \
   src/Pure/Admin/build_postgresql.scala \
   src/Pure/Admin/build_release.scala \
   src/Pure/Admin/build_scala.scala \
   src/Pure/Admin/build_spass.scala \
   src/Pure/Admin/build_sqlite.scala \
   src/Pure/Admin/build_status.scala \
   src/Pure/Admin/build_vampire.scala \
   src/Pure/Admin/build_verit.scala \
   src/Pure/Admin/build_zipperposition.scala \
   src/Pure/Admin/build_zstd.scala \
   src/Pure/Admin/check_sources.scala \
   src/Pure/Admin/ci_build.scala \
   src/Pure/Admin/isabelle_cronjob.scala \
   src/Pure/Admin/isabelle_devel.scala \
   src/Pure/Admin/jenkins.scala \
   src/Pure/Admin/other_isabelle.scala \
   src/Pure/Concurrent/consumer_thread.scala \
   src/Pure/Concurrent/counter.scala \
   src/Pure/Concurrent/delay.scala \
   src/Pure/Concurrent/event_timer.scala \
   src/Pure/Concurrent/future.scala \
   src/Pure/Concurrent/isabelle_thread.scala \
   src/Pure/Concurrent/mailbox.scala \
   src/Pure/Concurrent/par_list.scala \
   src/Pure/Concurrent/synchronized.scala \
   src/Pure/GUI/color_value.scala \
   src/Pure/GUI/desktop_app.scala \
   src/Pure/GUI/gui.scala \
   src/Pure/GUI/gui_thread.scala \
   src/Pure/GUI/popup.scala \
   src/Pure/GUI/wrap_panel.scala \
   src/Pure/General/antiquote.scala \
   src/Pure/General/base64.scala \
   src/Pure/General/bytes.scala \
   src/Pure/General/cache.scala \
   src/Pure/General/codepoint.scala \
   src/Pure/General/comment.scala \
   src/Pure/General/completion.scala \
   src/Pure/General/compress.scala \
   src/Pure/General/csv.scala \
   src/Pure/General/date.scala \
   src/Pure/General/exn.scala \
   src/Pure/General/file.scala \
   src/Pure/General/file_watcher.scala \
   src/Pure/General/graph.scala \
   src/Pure/General/graph_display.scala \
   src/Pure/General/graphics_file.scala \
   src/Pure/General/http.scala \
   src/Pure/General/json.scala \
   src/Pure/General/json_api.scala \
   src/Pure/General/linear_set.scala \
   src/Pure/General/logger.scala \
   src/Pure/General/long_name.scala \
   src/Pure/General/mailman.scala \
   src/Pure/General/mercurial.scala \
   src/Pure/General/multi_map.scala \
   src/Pure/General/output.scala \
   src/Pure/General/path.scala \
   src/Pure/General/position.scala \
   src/Pure/General/pretty.scala \
   src/Pure/General/properties.scala \
   src/Pure/General/rdf.scala \
   src/Pure/General/rsync.scala \
   src/Pure/General/scan.scala \
   src/Pure/General/sha1.scala \
   src/Pure/General/sql.scala \
   src/Pure/General/ssh.scala \
   src/Pure/General/symbol.scala \
   src/Pure/General/time.scala \
   src/Pure/General/timing.scala \
   src/Pure/General/untyped.scala \
   src/Pure/General/url.scala \
   src/Pure/General/utf8.scala \
   src/Pure/General/uuid.scala \
   src/Pure/General/value.scala \
   src/Pure/General/word.scala \
   src/Pure/General/zstd.scala \
   src/Pure/Isar/document_structure.scala \
   src/Pure/Isar/keyword.scala \
   src/Pure/Isar/line_structure.scala \
   src/Pure/Isar/outer_syntax.scala \
   src/Pure/Isar/parse.scala \
   src/Pure/Isar/token.scala \
   src/Pure/ML/ml_console.scala \
   src/Pure/ML/ml_lex.scala \
   src/Pure/ML/ml_process.scala \
   src/Pure/ML/ml_profiling.scala \
   src/Pure/ML/ml_statistics.scala \
   src/Pure/ML/ml_syntax.scala \
   src/Pure/PIDE/byte_message.scala \
   src/Pure/PIDE/command.scala \
   src/Pure/PIDE/command_span.scala \
   src/Pure/PIDE/document.scala \
   src/Pure/PIDE/document_id.scala \
   src/Pure/PIDE/document_info.scala \
   src/Pure/PIDE/document_status.scala \
   src/Pure/PIDE/editor.scala \
   src/Pure/PIDE/headless.scala \
   src/Pure/PIDE/line.scala \
   src/Pure/PIDE/markup.scala \
   src/Pure/PIDE/markup_tree.scala \
   src/Pure/PIDE/protocol.scala \
   src/Pure/PIDE/protocol_handlers.scala \
   src/Pure/PIDE/protocol_message.scala \
   src/Pure/PIDE/prover.scala \
   src/Pure/PIDE/query_operation.scala \
   src/Pure/PIDE/rendering.scala \
   src/Pure/PIDE/resources.scala \
   src/Pure/PIDE/session.scala \
   src/Pure/PIDE/text.scala \
   src/Pure/PIDE/xml.scala \
   src/Pure/PIDE/yxml.scala \
   src/Pure/ROOT.scala \
   src/Pure/System/bash.scala \
   src/Pure/System/classpath.scala \
   src/Pure/System/command_line.scala \
   src/Pure/System/components.scala \
   src/Pure/System/executable.scala \
   src/Pure/System/getopts.scala \
   src/Pure/System/isabelle_charset.scala \
   src/Pure/System/isabelle_fonts.scala \
   src/Pure/System/isabelle_platform.scala \
   src/Pure/System/isabelle_process.scala \
   src/Pure/System/isabelle_system.scala \
   src/Pure/System/isabelle_tool.scala \
   src/Pure/System/java_statistics.scala \
   src/Pure/System/linux.scala \
   src/Pure/System/mingw.scala \
   src/Pure/System/numa.scala \
   src/Pure/System/options.scala \
   src/Pure/System/platform.scala \
   src/Pure/System/posix_interrupt.scala \
   src/Pure/System/process_result.scala \
   src/Pure/System/progress.scala \
   src/Pure/System/scala.scala \
   src/Pure/System/system_channel.scala \
   src/Pure/System/tty_loop.scala \
   src/Pure/Thy/bibtex.scala \
   src/Pure/Thy/browser_info.scala \
   src/Pure/Thy/document_build.scala \
   src/Pure/Thy/export.scala \
   src/Pure/Thy/export_theory.scala \
   src/Pure/Thy/file_format.scala \
   src/Pure/Thy/html.scala \
   src/Pure/Thy/latex.scala \
   src/Pure/Thy/sessions.scala \
   src/Pure/Thy/thy_element.scala \
   src/Pure/Thy/thy_header.scala \
   src/Pure/Thy/thy_syntax.scala \
   src/Pure/Tools/build.scala \
   src/Pure/Tools/build_docker.scala \
   src/Pure/Tools/build_job.scala \
   src/Pure/Tools/check_keywords.scala \
   src/Pure/Tools/debugger.scala \
   src/Pure/Tools/doc.scala \
   src/Pure/Tools/dump.scala \
   src/Pure/Tools/flarum.scala \
   src/Pure/Tools/fontforge.scala \
   src/Pure/Tools/java_monitor.scala \
   src/Pure/Tools/logo.scala \
   src/Pure/Tools/mkroot.scala \
   src/Pure/Tools/phabricator.scala \
   src/Pure/Tools/print_operation.scala \
   src/Pure/Tools/profiling_report.scala \
   src/Pure/Tools/scala_build.scala \
   src/Pure/Tools/scala_project.scala \
   src/Pure/Tools/server.scala \
   src/Pure/Tools/server_commands.scala \
   src/Pure/Tools/simplifier_trace.scala \
   src/Pure/Tools/spell_checker.scala \
   src/Pure/Tools/sync.scala \
   src/Pure/Tools/task_statistics.scala \
   src/Pure/Tools/update.scala \
   src/Pure/Tools/update_cartouches.scala \
   src/Pure/Tools/update_comments.scala \
   src/Pure/Tools/update_header.scala \
   src/Pure/Tools/update_then.scala \
   src/Pure/Tools/update_theorems.scala \
   src/Pure/library.scala \
   src/Pure/pure_thy.scala \
   src/Pure/term.scala \
   src/Pure/term_xml.scala \
   src/Pure/thm_name.scala \
   src/Tools/Graphview/graph_file.scala \
   src/Tools/Graphview/graph_panel.scala \
   src/Tools/Graphview/graphview.scala \
   src/Tools/Graphview/layout.scala \
   src/Tools/Graphview/main_panel.scala \
   src/Tools/Graphview/metrics.scala \
   src/Tools/Graphview/model.scala \
   src/Tools/Graphview/mutator.scala \
   src/Tools/Graphview/mutator_dialog.scala \
   src/Tools/Graphview/mutator_event.scala \
   src/Tools/Graphview/popups.scala \
   src/Tools/Graphview/shapes.scala \
   src/Tools/Graphview/tree_panel.scala \
   src/Tools/VSCode/src/build_vscode_extension.scala \
   src/Tools/VSCode/src/build_vscodium.scala \
   src/Tools/VSCode/src/channel.scala \
   src/Tools/VSCode/src/dynamic_output.scala \
   src/Tools/VSCode/src/language_server.scala \
   src/Tools/VSCode/src/lsp.scala \
   src/Tools/VSCode/src/preview_panel.scala \
   src/Tools/VSCode/src/state_panel.scala \
   src/Tools/VSCode/src/vscode_main.scala \
   src/Tools/VSCode/src/vscode_model.scala \
   src/Tools/VSCode/src/vscode_rendering.scala \
   src/Tools/VSCode/src/vscode_resources.scala \
   src/Tools/VSCode/src/vscode_spell_checker.scala \
   src/Tools/jEdit/src/active.scala \
   src/Tools/jEdit/src/base_plugin.scala \
   src/Tools/jEdit/src/completion_popup.scala \
   src/Tools/jEdit/src/context_menu.scala \
   src/Tools/jEdit/src/debugger_dockable.scala \
   src/Tools/jEdit/src/dockable.scala \
   src/Tools/jEdit/src/document_dockable.scala \
   src/Tools/jEdit/src/document_model.scala \
   src/Tools/jEdit/src/document_view.scala \
   src/Tools/jEdit/src/documentation_dockable.scala \
   src/Tools/jEdit/src/fold_handling.scala \
   src/Tools/jEdit/src/font_info.scala \
   src/Tools/jEdit/src/graphview_dockable.scala \
   src/Tools/jEdit/src/info_dockable.scala \
   src/Tools/jEdit/src/isabelle.scala \
   src/Tools/jEdit/src/isabelle_encoding.scala \
   src/Tools/jEdit/src/isabelle_export.scala \
-  src/Tools/jEdit/src/isabelle_options.scala \
   src/Tools/jEdit/src/isabelle_session.scala \
   src/Tools/jEdit/src/isabelle_vfs.scala \
   src/Tools/jEdit/src/jedit_bibtex.scala \
   src/Tools/jEdit/src/jedit_editor.scala \
   src/Tools/jEdit/src/jedit_lib.scala \
   src/Tools/jEdit/src/jedit_main.scala \
   src/Tools/jEdit/src/jedit_options.scala \
   src/Tools/jEdit/src/jedit_plugins.scala \
   src/Tools/jEdit/src/jedit_rendering.scala \
   src/Tools/jEdit/src/jedit_resources.scala \
   src/Tools/jEdit/src/jedit_sessions.scala \
   src/Tools/jEdit/src/jedit_spell_checker.scala \
   src/Tools/jEdit/src/keymap_merge.scala \
   src/Tools/jEdit/src/main_plugin.scala \
   src/Tools/jEdit/src/monitor_dockable.scala \
   src/Tools/jEdit/src/output_dockable.scala \
   src/Tools/jEdit/src/pide_docking_framework.scala \
   src/Tools/jEdit/src/pretty_text_area.scala \
   src/Tools/jEdit/src/pretty_tooltip.scala \
   src/Tools/jEdit/src/process_indicator.scala \
   src/Tools/jEdit/src/protocol_dockable.scala \
   src/Tools/jEdit/src/query_dockable.scala \
   src/Tools/jEdit/src/raw_output_dockable.scala \
   src/Tools/jEdit/src/rich_text_area.scala \
   src/Tools/jEdit/src/session_build.scala \
   src/Tools/jEdit/src/simplifier_trace_dockable.scala \
   src/Tools/jEdit/src/simplifier_trace_window.scala \
   src/Tools/jEdit/src/sledgehammer_dockable.scala \
   src/Tools/jEdit/src/state_dockable.scala \
   src/Tools/jEdit/src/status_widget.scala \
   src/Tools/jEdit/src/symbols_dockable.scala \
   src/Tools/jEdit/src/syntax_style.scala \
   src/Tools/jEdit/src/syslog_dockable.scala \
   src/Tools/jEdit/src/text_overview.scala \
   src/Tools/jEdit/src/text_structure.scala \
   src/Tools/jEdit/src/theories_dockable.scala \
   src/Tools/jEdit/src/timing_dockable.scala \
   src/Tools/jEdit/src/token_markup.scala
 services = \
   isabelle.Bash$Handler \
   isabelle.Bibtex$File_Format \
   isabelle.Document_Build$Build_Engine \
   isabelle.Document_Build$LuaLaTeX_Engine \
   isabelle.Document_Build$PDFLaTeX_Engine \
   isabelle.CI_Builds \
   isabelle.ML_Statistics$Handler \
   isabelle.Print_Operation$Handler \
   isabelle.Scala$Handler \
   isabelle.Scala_Functions \
   isabelle.Server_Commands \
   isabelle.Sessions$File_Format \
   isabelle.Simplifier_Trace$Handler \
   isabelle.Tools \
   isabelle.jedit.JEdit_Plugin0 \
   isabelle.jedit.JEdit_Plugin1 \
   isabelle.nitpick.Kodkod$Handler \
   isabelle.nitpick.Scala_Functions \
   isabelle.spark.SPARK$Load_Command1 \
   isabelle.spark.SPARK$Load_Command2
diff --git a/src/Tools/jEdit/jedit_main/plugin.props b/src/Tools/jEdit/jedit_main/plugin.props
--- a/src/Tools/jEdit/jedit_main/plugin.props
+++ b/src/Tools/jEdit/jedit_main/plugin.props
@@ -1,114 +1,114 @@
 ## Isabelle/jEdit plugin properties
 ##
 ##:wrap=soft:maxLineLen=100:
 
 #identification
 plugin.isabelle.jedit_main.Plugin.name=Isabelle
 plugin.isabelle.jedit_main.Plugin.author=Johannes H\u00F6lzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel
 plugin.isabelle.jedit_main.Plugin.version=11.3
 plugin.isabelle.jedit_main.Plugin.description=Isabelle/jEdit main plugin
 
 #system parameters
 plugin.isabelle.jedit_main.Plugin.activate=defer
 plugin.isabelle.jedit_main.Plugin.usePluginHome=false
 
 #dependencies
 plugin.isabelle.jedit_main.Plugin.depend.0=jdk 11
 plugin.isabelle.jedit_main.Plugin.depend.1=jedit 05.06.00.00
 plugin.isabelle.jedit_main.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
 plugin.isabelle.jedit_main.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.4.0
 plugin.isabelle.jedit_main.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8
 plugin.isabelle.jedit_main.Plugin.depend.5=plugin isabelle.jedit_base.Plugin 1.0
 
 #options
 plugin.isabelle.jedit_main.Plugin.option-group=isabelle-general isabelle-rendering
 options.isabelle-general.label=General
-options.isabelle-general.code=new isabelle.jedit.Isabelle_Options1();
+options.isabelle-general.code=new isabelle.jedit.JEdit_Options$Isabelle_General_Options();
 options.isabelle-rendering.label=Rendering
-options.isabelle-rendering.code=new isabelle.jedit.Isabelle_Options2();
+options.isabelle-rendering.code=new isabelle.jedit.JEdit_Options$Isabelle_Rendering_Options();
 
 #menu actions and dockables
 plugin.isabelle.jedit_main.Plugin.menu.label=Isabelle
 plugin.isabelle.jedit_main.Plugin.menu= \
   isabelle-export-browser \
   isabelle-session-browser \
   isabelle.preview \
   isabelle.draft \
   isabelle.java-monitor \
   - \
   isabelle-debugger \
   isabelle-document \
   isabelle-documentation \
   isabelle-monitor \
   isabelle-output \
   isabelle-protocol \
   isabelle-query \
   isabelle-raw-output \
   isabelle-simplifier-trace \
   isabelle-sledgehammer \
   isabelle-state \
   isabelle-symbols \
   isabelle-syslog \
   isabelle-theories \
   isabelle-timing
 isabelle-debugger.label=Debugger panel
 isabelle-debugger.title=Debugger
 isabelle-document.label=Document panel
 isabelle-document.title=Document
 isabelle-documentation.label=Documentation panel
 isabelle-documentation.title=Documentation
 isabelle-graphview.label=Graphview panel
 isabelle-graphview.title=Graphview
 isabelle-info.label=Info panel
 isabelle-info.title=Info
 isabelle-monitor.label=Monitor panel
 isabelle-monitor.title=Monitor
 isabelle-output.label=Output panel
 isabelle-output.title=Output
 isabelle-protocol.label=Protocol panel
 isabelle-protocol.title=Protocol
 isabelle-query.label=Query panel
 isabelle-query.title=Query
 isabelle-raw-output.label=Raw Output panel
 isabelle-raw-output.title=Raw Output
 isabelle-simplifier-trace.label=Simplifier Trace panel
 isabelle-simplifier-trace.title=Simplifier Trace
 isabelle-sledgehammer.label=Sledgehammer panel
 isabelle-sledgehammer.title=Sledgehammer
 isabelle-state.label=State panel
 isabelle-state.title=State
 isabelle-symbols.label=Symbols panel
 isabelle-symbols.title=Symbols
 isabelle-syslog.label=Syslog panel
 isabelle-syslog.title=Syslog
 isabelle-theories.label=Theories panel
 isabelle-theories.title=Theories
 isabelle-timing.label=Timing panel
 isabelle-timing.title=Timing
 
 #SideKick
 mode.isabelle-news.folding=sidekick
 mode.isabelle-news.sidekick.parser=isabelle-news
 mode.isabelle-options.folding=sidekick
 mode.isabelle-options.sidekick.parser=isabelle-options
 mode.isabelle-root.folding=sidekick
 mode.isabelle-root.sidekick.parser=isabelle-root
 mode.isabelle.customSettings=true
 mode.isabelle.folding=isabelle
 mode.isabelle.sidekick.parser=isabelle
 mode.isabelle.sidekick.showStatusWindow.label=true
 mode.isabelle-ml.folding=sidekick
 mode.isabelle-ml.sidekick.parser=isabelle-ml
 mode.sml.folding=sidekick
 mode.sml.sidekick.parser=isabelle-sml
 mode.bibtex.folding=sidekick
 mode.bibtex.sidekick.parser=bibtex
 sidekick.parser.isabelle.label=isabelle
 sidekick.parser.isabelle-context.label=isabelle-context
 sidekick.parser.isabelle-markup.label=isabelle-markup
 sidekick.parser.isabelle-ml.label=isabelle-ml
 sidekick.parser.isabelle-sml.label=isabelle-sml
 sidekick.parser.isabelle-news.label=isabelle-news
 sidekick.parser.isabelle-options.label=isabelle-options
 sidekick.parser.isabelle-root.label=isabelle-root
 sidekick.parser.bibtex.label=bibtex
diff --git a/src/Tools/jEdit/src/isabelle_options.scala b/src/Tools/jEdit/src/isabelle_options.scala
deleted file mode 100644
--- a/src/Tools/jEdit/src/isabelle_options.scala
+++ /dev/null
@@ -1,61 +0,0 @@
-/*  Title:      Tools/jEdit/src/isabelle_options.scala
-    Author:     Makarius
-
-Editor pane for plugin options.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.{jEdit, AbstractOptionPane}
-
-
-abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) {
-  protected val components: List[(String, List[Option_Component])]
-
-  override def _init(): Unit = {
-    val dummy_property = "options.isabelle.dummy"
-
-    for ((s, cs) <- components) {
-      if (s.nonEmpty) {
-        jEdit.setProperty(dummy_property, s)
-        addSeparator(dummy_property)
-        jEdit.setProperty(dummy_property, null)
-      }
-      for (c <- cs) addComponent(c.title, c.peer)
-    }
-  }
-
-  override def _save(): Unit = {
-    for ((_, cs) <- components; c <- cs) c.save()
-  }
-}
-
-
-class Isabelle_Options1 extends Isabelle_Options("isabelle-general") {
-  val options: JEdit_Options = PIDE.options
-
-  private val predefined =
-    List(JEdit_Sessions.logic_selector(options),
-      JEdit_Spell_Checker.dictionaries_selector())
-
-  protected val components: List[(String, List[Option_Component])] =
-    options.make_components(predefined,
-      (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet)
-}
-
-
-class Isabelle_Options2 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)
-    } yield PIDE.options.make_color_component(opt)).toList
-
-  assert(predefined.nonEmpty)
-
-  protected val components: List[(String, List[Option_Component])] =
-    PIDE.options.make_components(predefined, _ => false)
-}
diff --git a/src/Tools/jEdit/src/jedit_options.scala b/src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala
+++ b/src/Tools/jEdit/src/jedit_options.scala
@@ -1,165 +1,216 @@
 /*  Title:      Tools/jEdit/src/jedit_options.scala
     Author:     Makarius
 
 Options for Isabelle/jEdit.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.awt.{Font, Color}
 import javax.swing.{InputVerifier, JComponent, UIManager}
 import javax.swing.text.JTextComponent
 
 import scala.swing.{Component, CheckBox, TextArea}
 
 import org.gjt.sp.jedit.gui.ColorWellButton
+import org.gjt.sp.jedit.{jEdit, AbstractOptionPane}
 
 
 trait Option_Component extends Component {
   val title: String
   def load(): Unit
   def save(): Unit
 }
 
 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) {
     def apply(): A = access.apply(name)
     def update(x: A): Unit = change(_ => x)
     def change(f: A => A): Unit = {
       val x0 = apply()
       access.change(name, f)
       val x1 = apply()
       if (x0 != x1) changed()
     }
     def changed(): Unit = GUI_Thread.require { PIDE.session.update_options(access.options.value) }
   }
 
   class Bool_Access(name: String) extends Access(PIDE.options.bool, name) {
     def set(): Unit = update(true)
     def reset(): Unit = update(false)
     def toggle(): Unit = change(b => !b)
   }
 
   class Bool_GUI(access: Bool_Access, label: String)
   extends GUI.Check(label, init = access()) {
     def load(): Unit = { selected = access() }
     override def clicked(state: Boolean): Unit = access.update(state)
   }
 
 
   /* specific options */
 
   object continuous_checking extends Bool_Access("editor_continuous_checking") {
     override def changed(): Unit = {
       super.changed()
       PIDE.plugin.deps_changed()
     }
 
     class GUI extends Bool_GUI(this, "Continuous checking") {
       tooltip = "Continuous checking of proof document (visible and required parts)"
     }
   }
 
   object output_state extends Bool_Access("editor_output_state") {
     override def changed(): Unit = GUI_Thread.require {
       super.changed()
       PIDE.editor.flush_edits(hidden = true)
       PIDE.editor.flush()
     }
 
     class GUI extends Bool_GUI(this, "Proof state") {
       tooltip = "Output of proof state (normally shown on State panel)"
     }
   }
+
+
+  /* editor pane for plugin options */
+
+  abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) {
+    protected val components: List[(String, List[Option_Component])]
+
+    override def _init(): Unit = {
+      val dummy_property = "options.isabelle.dummy"
+
+      for ((s, cs) <- components) {
+        if (s.nonEmpty) {
+          jEdit.setProperty(dummy_property, s)
+          addSeparator(dummy_property)
+          jEdit.setProperty(dummy_property, null)
+        }
+        for (c <- cs) addComponent(c.title, c.peer)
+      }
+    }
+
+    override def _save(): Unit = {
+      for ((_, cs) <- components; c <- cs) c.save()
+    }
+  }
+
+
+  class Isabelle_General_Options extends Isabelle_Options("isabelle-general") {
+    val options: JEdit_Options = PIDE.options
+
+    private val predefined =
+      List(JEdit_Sessions.logic_selector(options),
+        JEdit_Spell_Checker.dictionaries_selector())
+
+    protected val components: List[(String, List[Option_Component])] =
+      options.make_components(predefined,
+        (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)
+      } yield PIDE.options.make_color_component(opt)).toList
+
+    assert(predefined.nonEmpty)
+
+    protected val components: List[(String, List[Option_Component])] =
+      PIDE.options.make_components(predefined, _ => false)
+  }
 }
 
 class JEdit_Options(init_options: Options) extends Options_Variable(init_options) {
   def color_value(s: String): Color = Color_Value(string(s))
 
   def make_color_component(opt: Options.Opt): Option_Component = {
     GUI_Thread.require {}
 
     val opt_name = opt.name
     val opt_title = opt.title("jedit")
 
     val button = new ColorWellButton(Color_Value(opt.value))
     val component = new Component with Option_Component {
       override lazy val peer: JComponent = button
       name = opt_name
       val title: String = opt_title
       def load(): Unit = button.setSelectedColor(Color_Value(string(opt_name)))
       def save(): Unit = string(opt_name) = Color_Value.print(button.getSelectedColor)
     }
     component.tooltip = GUI.tooltip_lines(opt.print_default)
     component
   }
 
   def make_component(opt: Options.Opt): Option_Component = {
     GUI_Thread.require {}
 
     val opt_name = opt.name
     val opt_title = opt.title("jedit")
 
     val component =
       if (opt.typ == Options.Bool)
         new CheckBox with Option_Component {
           name = opt_name
           val title: String = opt_title
           def load(): Unit = selected = bool(opt_name)
           def save(): Unit = bool(opt_name) = selected
         }
       else {
         val default_font = GUI.copy_font(UIManager.getFont("TextField.font"))
         val text_area =
           new TextArea with Option_Component {
             if (default_font != null) font = default_font
             name = opt_name
             val title: String = opt_title
             def load(): Unit = text = value.check_name(opt_name).value
             def save(): Unit =
               try { JEdit_Options.this += (opt_name, text) }
               catch {
                 case ERROR(msg) =>
                   GUI.error_dialog(this.peer, "Failed to update options",
                     GUI.scrollable_text(msg))
               }
           }
         text_area.peer.setInputVerifier({
             case text: JTextComponent =>
               try { value + (opt_name, text.getText); true }
               catch { case ERROR(_) => false }
             case _ => true
           })
         GUI.plain_focus_traversal(text_area.peer)
         text_area
       }
     component.load()
     component.tooltip = GUI.tooltip_lines(opt.print_default)
     component
   }
 
   def make_components(
     predefined: List[Option_Component],
     filter: String => Boolean
   ) : List[(String, List[Option_Component])] = {
     def mk_component(opt: Options.Opt): List[Option_Component] =
       predefined.find(opt.name == _.name) match {
         case Some(c) => List(c)
         case None => if (filter(opt.name)) List(make_component(opt)) else Nil
       }
     value.sections.sortBy(_._1).map(
         { case (a, opts) => (a, opts.sortBy(_.title("jedit")).flatMap(mk_component)) })
       .filterNot(_._2.isEmpty)
   }
 }
-