src/Tools/jEdit/src/simplifier_trace_dockable.scala

--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -36,7 +36,7 @@
   private val text_area = new Pretty_Text_Area(view)
   set_content(text_area)
 
-  private def update_contents()
+  private def update_contents(): Unit =
   {
     val snapshot = current_snapshot
     val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
@@ -62,25 +62,22 @@
     do_paint()
   }
 
-  private def show_trace()
+  private def show_trace(): Unit =
   {
     val trace = Simplifier_Trace.generate_trace(PIDE.session, current_results)
     new Simplifier_Trace_Window(view, current_snapshot, trace)
   }
 
-  private def do_paint()
+  private def do_paint(): Unit =
   {
     GUI_Thread.later {
       text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
     }
   }
 
-  private def handle_resize()
-  {
-    do_paint()
-  }
+  private def handle_resize(): Unit = do_paint()
 
-  private def handle_update(follow: Boolean)
+  private def handle_update(follow: Boolean): Unit =
   {
     val (new_snapshot, new_command, new_results, new_id) =
       PIDE.editor.current_node_snapshot(view) match {
@@ -122,7 +119,7 @@
         GUI_Thread.later { handle_update(do_update) }
     }
 
-  override def init()
+  override def init(): Unit =
   {
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
@@ -131,7 +128,7 @@
     handle_update(true)
   }
 
-  override def exit()
+  override def exit(): Unit =
   {
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
@@ -147,8 +144,8 @@
     Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
-    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
   })