diff --git a/src/Tools/jEdit/src/isabelle_options.scala b/src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala
+++ b/src/Tools/jEdit/src/isabelle_options.scala
@@ -1,60 +1,61 @@
 /*  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 != "") {
         jEdit.setProperty(dummy_property, s)
         addSeparator(dummy_property)
         jEdit.setProperty(dummy_property, null)
       }
       cs.foreach(c => addComponent(c.title, c.peer))
     }
   }
 
   override def _save(): Unit = {
     for ((_, cs) <- components) cs.foreach(_.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 =
+  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 = PIDE.options.make_components(predefined, _ => false)
+  protected val components: List[(String, List[Option_Component])] =
+    PIDE.options.make_components(predefined, _ => false)
 }