--- 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 =
--- 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
--- 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))