tuned;

--- a/src/Tools/jEdit/src/isabelle_options.scala	Fri Oct 28 15:42:59 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Fri Oct 28 15:46:20 2022 +0200
@@ -19,17 +19,17 @@
     val dummy_property = "options.isabelle.dummy"
 
     for ((s, cs) <- components) {
-      if (s != "") {
+      if (s.nonEmpty) {
         jEdit.setProperty(dummy_property, s)
         addSeparator(dummy_property)
         jEdit.setProperty(dummy_property, null)
       }
-      cs.foreach(c => addComponent(c.title, c.peer))
+      for (c <- cs) addComponent(c.title, c.peer)
     }
   }
 
   override def _save(): Unit = {
-    for ((_, cs) <- components) cs.foreach(_.save())
+    for ((_, cs) <- components; c <- cs) c.save()
   }
 }