src/Tools/VSCode/src/state_panel.scala

--- a/src/Tools/VSCode/src/state_panel.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/VSCode/src/state_panel.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -15,14 +15,14 @@
   private val make_id = Counter.make()
   private val instances = Synchronized(Map.empty[Counter.ID, State_Panel])
 
-  def init(server: Language_Server)
+  def init(server: Language_Server): Unit =
   {
     val instance = new State_Panel(server)
     instances.change(_ + (instance.id -> instance))
     instance.init()
   }
 
-  def exit(id: Counter.ID)
+  def exit(id: Counter.ID): Unit =
   {
     instances.change(map =>
       map.get(id) match {
@@ -74,9 +74,9 @@
           output(content)
         })
 
-  def locate() { print_state.locate_query() }
+  def locate(): Unit = print_state.locate_query()
 
-  def update()
+  def update(): Unit =
   {
     server.editor.current_node_snapshot(()) match {
       case Some(snapshot) =>
@@ -93,7 +93,7 @@
 
   private val auto_update_enabled = Synchronized(true)
 
-  def auto_update(set: Option[Boolean] = None)
+  def auto_update(set: Option[Boolean] = None): Unit =
   {
     val enabled =
       auto_update_enabled.guarded_access(a =>
@@ -155,7 +155,7 @@
         auto_update()
     }
 
-  def init()
+  def init(): Unit =
   {
     server.session.commands_changed += main
     server.session.caret_focus += main
@@ -163,7 +163,7 @@
     server.editor.send_dispatcher { auto_update() }
   }
 
-  def exit()
+  def exit(): Unit =
   {
     output_active.change(_ => false)
     server.session.commands_changed -= main