# HG changeset patch
# User wenzelm
# Date 1666964579 -7200
# Node ID 03b4bb973d88d1660cb666baf86f3142663cff3d
# Parent  5ca3391244a3072550c32d83bc74848d9357ae5b
tuned signature, following hints by IntelliJ IDEA;

diff -r 5ca3391244a3 -r 03b4bb973d88 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Fri Oct 28 13:18:27 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Fri Oct 28 15:42:59 2022 +0200
@@ -41,7 +41,7 @@
     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)
 }
@@ -56,5 +56,6 @@
 
   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)
 }