--- a/src/Tools/jEdit/src/jedit_sessions.scala Sun Dec 18 15:49:37 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Sun Dec 18 15:50:51 2022 +0100
@@ -94,7 +94,7 @@
load()
}
- def logic_selector(options: Options_Variable, standalone: Boolean = false): JEdit_Options.Entry =
+ def logic_selector(options: Options_Variable, standalone: Boolean = false): Selector =
GUI_Thread.require {
val sessions = sessions_structure(options = options.value)
val all_sessions = sessions.imports_topological_order
@@ -108,7 +108,7 @@
all_sessions.sorted.map(GUI.Selector.item))
}
- def document_selector(options: Options_Variable, standalone: Boolean = false): JEdit_Options.Entry =
+ def document_selector(options: Options_Variable, standalone: Boolean = false): Selector =
GUI_Thread.require {
val sessions = sessions_structure(options = options.value)
val all_sessions = sessions.build_topological_order.sorted