--- a/src/Tools/VSCode/src/dynamic_output.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/VSCode/src/dynamic_output.scala Mon Mar 01 22:22:12 2021 +0100
@@ -50,8 +50,8 @@
{
private val state = Synchronized(Dynamic_Output.State())
- private def handle_update(restriction: Option[Set[Command]])
- { state.change(_.handle_update(server.resources, server.channel, restriction)) }
+ private def handle_update(restriction: Option[Set[Command]]): Unit =
+ state.change(_.handle_update(server.resources, server.channel, restriction))
/* main */
@@ -65,14 +65,14 @@
handle_update(None)
}
- def init()
+ def init(): Unit =
{
server.session.commands_changed += main
server.session.caret_focus += main
handle_update(None)
}
- def exit()
+ def exit(): Unit =
{
server.session.commands_changed -= main
server.session.caret_focus -= main