# HG changeset patch
# User wenzelm
# Date 1497645499 -7200
# Node ID d1639e7877cc3e6434c708a70a5748fd5970146d
# Parent  5aa9cb83e70e1634f62b36099e3e7d1e96590ee1
tuned;

diff -r 5aa9cb83e70e -r d1639e7877cc src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Fri Jun 16 21:04:39 2017 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Fri Jun 16 22:38:19 2017 +0200
@@ -90,15 +90,18 @@
 
   def set_auto_update(b: Boolean) { auto_update_enabled.change(_ => b); if (b) update() }
 
-  def auto_update(): Unit = if (auto_update_enabled.value) update()
+  def auto_update() { if (auto_update_enabled.value) update() }
 
 
   /* main */
 
   private val main =
     Session.Consumer[Any](getClass.getName) {
-      case changed: Session.Commands_Changed => if (changed.assignment) auto_update()
-      case Session.Caret_Focus => auto_update()
+      case changed: Session.Commands_Changed =>
+        if (changed.assignment) auto_update()
+
+      case Session.Caret_Focus =>
+        auto_update()
     }
 
   def init()