# HG changeset patch
# User wenzelm
# Date 1671375051 -3600
# Node ID fdaa17402af32d97779d3fef23f7af1de8ede6a7
# Parent  f34b923ff2c9f3376da23ec1fa0100d097ddd721
clarified signature;

diff -r f34b923ff2c9 -r fdaa17402af3 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