# HG changeset patch # User wenzelm # Date 1670340229 -3600 # Node ID 06b001094ddb421a6be4582edff198944fb5b12a # Parent c662a56e77a87f54b1001dd3b263972a99309191 more uniform session selectors, with persistent options; diff -r c662a56e77a8 -r 06b001094ddb etc/options --- a/etc/options Tue Dec 06 14:41:13 2022 +0100 +++ b/etc/options Tue Dec 06 16:23:49 2022 +0100 @@ -220,6 +220,9 @@ public option editor_output_state : bool = false -- "implicit output of proof state" +public option editor_document_session : string = "" + -- "session for interactive document preparation" + option editor_execution_delay : real = 0.02 -- "delay for start of execution process after document update (seconds)" diff -r c662a56e77a8 -r 06b001094ddb src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Tue Dec 06 14:41:13 2022 +0100 +++ b/src/Tools/jEdit/etc/options Tue Dec 06 16:23:49 2022 +0100 @@ -1,7 +1,7 @@ (* :mode=isabelle-options: *) public option jedit_logic : string = "" - -- "default logic session" + -- "logic session name (change requires restart)" public option jedit_print_mode : string = "" -- "default print modes for output, separated by commas (change requires restart)" diff -r c662a56e77a8 -r 06b001094ddb src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Tue Dec 06 14:41:13 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Tue Dec 06 16:23:49 2022 +0100 @@ -191,14 +191,8 @@ /* controls */ - private val document_session: GUI.Selector[String] = { - val sessions = JEdit_Sessions.sessions_structure() - val all_sessions = sessions.build_topological_order.sorted.map(GUI.Selector.item) - val doc_sessions = - for (entry <- all_sessions; name <- entry.get_value if sessions(name).doc_group) - yield entry - new GUI.Selector[String](doc_sessions, all_sessions) { val title = "Session" } - } + private val document_session = + JEdit_Sessions.document_selector(PIDE.options, autosave = true) private val build_button = new GUI.Button("Build") { @@ -261,6 +255,7 @@ Session.Consumer[Any](getClass.getName) { case _: Session.Global_Options => GUI_Thread.later { + document_session.load() handle_resize() theories.reinit() } diff -r c662a56e77a8 -r 06b001094ddb src/Tools/jEdit/src/jedit_options.scala --- a/src/Tools/jEdit/src/jedit_options.scala Tue Dec 06 14:41:13 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_options.scala Tue Dec 06 16:23:49 2022 +0100 @@ -106,7 +106,9 @@ val options: JEdit_Options = PIDE.options private val predefined = - List(JEdit_Sessions.logic_selector(options), + List( + JEdit_Sessions.logic_selector(options), + JEdit_Sessions.document_selector(options), JEdit_Spell_Checker.dictionaries_selector()) protected val components: List[(String, List[Entry])] = diff -r c662a56e77a8 -r 06b001094ddb src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Tue Dec 06 14:41:13 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Tue Dec 06 16:23:49 2022 +0100 @@ -67,37 +67,55 @@ else Position.none - /* logic selector */ + /* session selectors */ - def logic_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = { - GUI_Thread.require {} + class Selector( + val options: Options_Variable, + val option_name: String, + autosave: Boolean, + batches: List[GUI.Selector.Entry[String]]*) + extends GUI.Selector[String](batches: _*) with JEdit_Options.Entry { + name = option_name + tooltip = Word.capitalize(options.value.description(option_name)) - val sessions = sessions_structure(options = options.value) - val all_sessions = sessions.imports_topological_order - val main_sessions = all_sessions.filter(name => sessions(name).main_group) + override val title: String = + options.value.check_name(option_name).title("jedit") + override def load(): Unit = { + val value = options.string(option_name) + for (entry <- find_value(_ == value)) selection.item = entry + } + override def save(): Unit = + for (value <- selection_value) options.string(option_name) = value - val default_entry = - GUI.Selector.item_description("", "default (" + logic_name(options.value) + ")") + override def changed(): Unit = if (autosave) save() + + load() + } - new GUI.Selector[String]( - default_entry :: main_sessions.map(GUI.Selector.item), - all_sessions.sorted.map(GUI.Selector.item) - ) with JEdit_Options.Entry { - name = jedit_logic_option - tooltip = "Logic session name (change requires restart)" - val title = "Logic" - def load(): Unit = { - val logic = options.string(jedit_logic_option) - for (entry <- find_value(_ == logic)) selection.item = entry - } - def save(): Unit = - for (logic <- selection_value) options.string(jedit_logic_option) = logic + def logic_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = + GUI_Thread.require { + val sessions = sessions_structure(options = options.value) + val all_sessions = sessions.imports_topological_order + val main_sessions = all_sessions.filter(name => sessions(name).main_group) + + val default_entry = + GUI.Selector.item_description("", "default (" + logic_name(options.value) + ")") - override def changed(): Unit = if (autosave) save() + new Selector(options, jedit_logic_option, autosave, + default_entry :: main_sessions.map(GUI.Selector.item), + all_sessions.sorted.map(GUI.Selector.item)) + } - load() + def document_selector(options: Options_Variable, autosave: 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, + doc_sessions.map(GUI.Selector.item), + all_sessions.map(GUI.Selector.item)) } - } /* session build process */