# HG changeset patch
# User wenzelm
# Date 1666964780 -7200
# Node ID f70fcdc4cb43d4bee5cffbb537517fc5ed381b77
# Parent  03b4bb973d88d1660cb666baf86f3142663cff3d
tuned;

diff -r 03b4bb973d88 -r f70fcdc4cb43 src/Tools/jEdit/src/isabelle_options.scala
--- 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()
   }
 }