clarified signature;
authorwenzelm
Sun, 18 Dec 2022 15:50:51 +0100
changeset 76679 fdaa17402af3
parent 76678 f34b923ff2c9
child 76680 e95b9c9e17ff
clarified signature;
src/Tools/jEdit/src/jedit_sessions.scala
--- 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