--- 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)"
--- 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)"
--- 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("<html><b>Build</b></html>") {
@@ -261,6 +255,7 @@
Session.Consumer[Any](getClass.getName) {
case _: Session.Global_Options =>
GUI_Thread.later {
+ document_session.load()
handle_resize()
theories.reinit()
}
--- 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])] =
--- 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 */