# HG changeset patch # User wenzelm # Date 1509552463 -3600 # Node ID 58b166fd84474c6bd2fe91698419802273429133 # Parent 0525320d8774abb8b00778977ea450c23de00347 tuned; diff -r 0525320d8774 -r 58b166fd8447 src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Wed Nov 01 17:03:32 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Wed Nov 01 17:07:43 2017 +0100 @@ -53,7 +53,54 @@ else Position.none - /* session base info */ + /* logic selector */ + + private class Logic_Entry(val name: String, val description: String) + { + override def toString: String = description + } + + def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component = + { + GUI_Thread.require {} + + val session_list = + { + val sessions = Sessions.load(options.value, dirs = session_dirs()) + val (main_sessions, other_sessions) = + sessions.imports_topological_order.partition(info => info.groups.contains("main")) + main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted + } + + val entries = + 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 { + name = jedit_logic_option + val title = "Logic" + def load: Unit = + { + val logic = options.string(jedit_logic_option) + entries.find(_.name == logic) match { + case Some(entry) => selection.item = entry + case None => + } + } + def save: Unit = options.string(jedit_logic_option) = selection.item.name + } + + component.load() + if (autosave) { + component.listenTo(component.selection) + component.reactions += { case SelectionChanged(_) => component.save() } + } + component.tooltip = "Logic session name (change requires restart)" + component + } + + + /* session build process */ def session_base_info(options: Options): Sessions.Base_Info = { @@ -88,51 +135,4 @@ space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse, phase_changed = PIDE.plugin.session_phase_changed) } - - def session_list(options: Options): List[String] = - { - val sessions = Sessions.load(options, dirs = session_dirs()) - val (main_sessions, other_sessions) = - sessions.imports_topological_order.partition(info => info.groups.contains("main")) - main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted - } - - - /* logic selector */ - - private class Logic_Entry(val name: String, val description: String) - { - override def toString: String = description - } - - def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component = - { - GUI_Thread.require {} - - val entries = - new Logic_Entry("", "default (" + logic_name(options.value) + ")") :: - session_list(options.value).map(name => new Logic_Entry(name, name)) - - val component = new ComboBox(entries) with Option_Component { - name = jedit_logic_option - val title = "Logic" - def load: Unit = - { - val logic = options.string(jedit_logic_option) - entries.find(_.name == logic) match { - case Some(entry) => selection.item = entry - case None => - } - } - def save: Unit = options.string(jedit_logic_option) = selection.item.name - } - - component.load() - if (autosave) { - component.listenTo(component.selection) - component.reactions += { case SelectionChanged(_) => component.save() } - } - component.tooltip = "Logic session name (change requires restart)" - component - } }