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