equal
deleted
inserted
replaced
78 val session_entries = { |
78 val session_entries = { |
79 val sessions = sessions_structure(options = options.value) |
79 val sessions = sessions_structure(options = options.value) |
80 val all_sessions = sessions.imports_topological_order |
80 val all_sessions = sessions.imports_topological_order |
81 val main_sessions = all_sessions.filter(name => sessions(name).main_group) |
81 val main_sessions = all_sessions.filter(name => sessions(name).main_group) |
82 |
82 |
83 main_sessions.map(GUI.Selector.item) ::: List(GUI.Selector.separator) ::: |
83 main_sessions.map(GUI.Selector.item(_)) ::: List(GUI.Selector.separator()) ::: |
84 all_sessions.sorted.map(GUI.Selector.item) |
84 all_sessions.sorted.map(GUI.Selector.item(_, batch = 1)) |
85 } |
85 } |
86 |
86 |
87 new GUI.Selector(default_entry :: session_entries) with JEdit_Options.Entry { |
87 new GUI.Selector(default_entry :: session_entries) with JEdit_Options.Entry { |
88 name = jedit_logic_option |
88 name = jedit_logic_option |
89 tooltip = "Logic session name (change requires restart)" |
89 tooltip = "Logic session name (change requires restart)" |
90 val title = "Logic" |
90 val title = "Logic" |
91 def load(): Unit = { |
91 def load(): Unit = { |
92 val logic = options.string(jedit_logic_option) |
92 val logic = options.string(jedit_logic_option) |
93 entries.find { case GUI.Selector.Item(item, _) => item == logic case _ => false } match { |
93 entries.find { |
|
94 case item: GUI.Selector.Item[_] => item.item == logic |
|
95 case _ => false |
|
96 } match { |
94 case Some(entry) => selection.item = entry |
97 case Some(entry) => selection.item = entry |
95 case None => |
98 case None => |
96 } |
99 } |
97 } |
100 } |
98 def save(): Unit = |
101 def save(): Unit = |