tuned;
authorwenzelm
Fri, 12 Aug 2022 20:05:21 +0200
changeset 75828 298707451ec2
parent 75827 4920ebbde486
child 75829 b8a4f9b1eed6
tuned;
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
   }