--- 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
}