# HG changeset patch # User wenzelm # Date 1660328060 -7200 # Node ID b8a4f9b1eed622d82a3f5d43b07d63cd370372eb # Parent 298707451ec20b3a312ddfdb4e6012978cc593e5 clarified signature; diff -r 298707451ec2 -r b8a4f9b1eed6 src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Fri Aug 12 20:05:21 2022 +0200 +++ b/src/Tools/jEdit/src/isabelle_options.scala Fri Aug 12 20:14:20 2022 +0200 @@ -38,7 +38,7 @@ val options: JEdit_Options = PIDE.options private val predefined = - List(JEdit_Sessions.logic_selector(options, false), + List(JEdit_Sessions.logic_selector(options), JEdit_Spell_Checker.dictionaries_selector()) protected val components = diff -r 298707451ec2 -r b8a4f9b1eed6 src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Aug 12 20:05:21 2022 +0200 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Aug 12 20:14:20 2022 +0200 @@ -72,23 +72,23 @@ /* logic selector */ - private class Logic_Entry(val name: String, val description: String) { - override def toString: String = description + private sealed case class Logic_Entry(name: String = "", description: String = "") { + override def toString: String = proper_string(description) getOrElse name } - def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component = { + def logic_selector(options: Options_Variable, autosave: Boolean = false): Option_Component = { GUI_Thread.require {} - val session_list = { + val default_entry = Logic_Entry(description = "default (" + logic_name(options.value) + ")") + + val session_entries = { val sessions = sessions_structure(options = options.value) val (main_sessions, other_sessions) = sessions.imports_topological_order.partition(name => sessions(name).groups.contains("main")) - main_sessions.sorted ::: other_sessions.sorted + (main_sessions.sorted ::: other_sessions.sorted).map(name => Logic_Entry(name = name)) } - val entries = - new Logic_Entry("", "default (" + logic_name(options.value) + ")") :: - session_list.map(name => new Logic_Entry(name, name)) + val entries = default_entry :: session_entries new ComboBox(entries) with Option_Component { name = jedit_logic_option diff -r 298707451ec2 -r b8a4f9b1eed6 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Fri Aug 12 20:05:21 2022 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Fri Aug 12 20:14:20 2022 +0200 @@ -83,7 +83,7 @@ private val continuous_checking = new Isabelle.Continuous_Checking continuous_checking.focusable = false - private val logic = JEdit_Sessions.logic_selector(PIDE.options, true) + private val logic = JEdit_Sessions.logic_selector(PIDE.options, autosave = true) private val controls = Wrap_Panel(List(purge, continuous_checking, session_phase, logic))