src/Tools/jEdit/src/text_overview.scala
changeset 73340 0ffcad1f6130
parent 71704 b9a5eb0f3b43
child 73367 77ef8bef0593
--- a/src/Tools/jEdit/src/text_overview.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -33,19 +33,22 @@
   setRequestFocusEnabled(false)
 
   addMouseListener(new MouseAdapter {
-    override def mousePressed(event: MouseEvent) {
+    override def mousePressed(event: MouseEvent): Unit =
+    {
       val line = (event.getY * lines()) / getHeight
       if (line >= 0 && line < text_area.getLineCount)
         text_area.setCaretPosition(text_area.getLineStartOffset(line))
     }
   })
 
-  override def addNotify() {
+  override def addNotify(): Unit =
+  {
     super.addNotify()
     ToolTipManager.sharedInstance.registerComponent(this)
   }
 
-  override def removeNotify() {
+  override def removeNotify(): Unit =
+  {
     ToolTipManager.sharedInstance.unregisterComponent(this)
     super.removeNotify
   }
@@ -77,7 +80,7 @@
   private val delay_repaint =
     Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { repaint() }
 
-  override def paintComponent(gfx: Graphics)
+  override def paintComponent(gfx: Graphics): Unit =
   {
     super.paintComponent(gfx)
     GUI_Thread.assert {}