src/Tools/VSCode/src/dynamic_output.scala

 
 class Dynamic_Output private(server: Language_Server)
 {
   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 */
 
   private val main =

 
       case Session.Caret_Focus =>
         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
   }
 }