# 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