# HG changeset patch # User wenzelm # Date 1670341130 -3600 # Node ID 699d9a219e4509b66a335116cc91222ef930242f # Parent c79b43c1c7abb5c3938b6f60343c37ba8d24e2da tuned signature; diff -r c79b43c1c7ab -r 699d9a219e45 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Tue Dec 06 16:26:59 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Tue Dec 06 16:38:50 2022 +0100 @@ -192,7 +192,7 @@ /* controls */ private val document_session = - JEdit_Sessions.document_selector(PIDE.options, autosave = true) + JEdit_Sessions.document_selector(PIDE.options, standalone = true) private val build_button = new GUI.Button("Build") { diff -r c79b43c1c7ab -r 699d9a219e45 src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Tue Dec 06 16:26:59 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Tue Dec 06 16:38:50 2022 +0100 @@ -72,7 +72,7 @@ class Selector( val options: Options_Variable, val option_name: String, - autosave: Boolean, + standalone: Boolean, batches: List[GUI.Selector.Entry[String]]*) extends GUI.Selector[String](batches: _*) with JEdit_Options.Entry { name = option_name @@ -87,12 +87,12 @@ override def save(): Unit = for (value <- selection_value) options.string(option_name) = value - override def changed(): Unit = if (autosave) save() + override def changed(): Unit = if (standalone) save() load() } - def logic_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = + def logic_selector(options: Options_Variable, standalone: Boolean = false): JEdit_Options.Entry = GUI_Thread.require { val sessions = sessions_structure(options = options.value) val all_sessions = sessions.imports_topological_order @@ -101,18 +101,18 @@ val default_entry = GUI.Selector.item_description("", "default (" + logic_name(options.value) + ")") - new Selector(options, jedit_logic_option, autosave, + new Selector(options, jedit_logic_option, standalone, default_entry :: main_sessions.map(GUI.Selector.item), all_sessions.sorted.map(GUI.Selector.item)) } - def document_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = + def document_selector(options: Options_Variable, standalone: Boolean = false): JEdit_Options.Entry = GUI_Thread.require { val sessions = sessions_structure(options = options.value) val all_sessions = sessions.build_topological_order.sorted val doc_sessions = all_sessions.filter(name => sessions(name).doc_group) - new Selector(options, "editor_document_session", autosave, + new Selector(options, "editor_document_session", standalone, doc_sessions.map(GUI.Selector.item), all_sessions.map(GUI.Selector.item)) } diff -r c79b43c1c7ab -r 699d9a219e45 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Tue Dec 06 16:26:59 2022 +0100 +++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Dec 06 16:38:50 2022 +0100 @@ -38,7 +38,7 @@ private val continuous_checking = new JEdit_Options.continuous_checking.GUI continuous_checking.focusable = false - private val logic = JEdit_Sessions.logic_selector(PIDE.options, autosave = true) + private val logic = JEdit_Sessions.logic_selector(PIDE.options, standalone = true) private val controls = Wrap_Panel(List(purge, continuous_checking, session_phase, logic))