# HG changeset patch
# User wenzelm
# Date 1660327521 -7200
# Node ID 298707451ec20b3a312ddfdb4e6012978cc593e5
# Parent  4920ebbde4869b68b3492cfb94b967f2d5cd805c
tuned;

diff -r 4920ebbde486 -r 298707451ec2 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Aug 12 19:47:38 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Aug 12 20:05:21 2022 +0200
@@ -90,8 +90,9 @@
       new Logic_Entry("", "default (" + logic_name(options.value) + ")") ::
         session_list.map(name => new Logic_Entry(name, name))
 
-    val component = new ComboBox(entries) with Option_Component {
+    new ComboBox(entries) with Option_Component {
       name = jedit_logic_option
+      tooltip = "Logic session name (change requires restart)"
       val title = "Logic"
       def load(): Unit = {
         val logic = options.string(jedit_logic_option)
@@ -101,15 +102,13 @@
         }
       }
       def save(): Unit = options.string(jedit_logic_option) = selection.item.name
+
+      load()
+      if (autosave) {
+        listenTo(selection)
+        reactions += { case SelectionChanged(_) => save() }
+      }
     }
-
-    component.load()
-    if (autosave) {
-      component.listenTo(component.selection)
-      component.reactions += { case SelectionChanged(_) => component.save() }
-    }
-    component.tooltip = "Logic session name (change requires restart)"
-    component
   }