# HG changeset patch
# User wenzelm
# Date 1660297661 -7200
# Node ID 74d6d09e1a363a8d90af651f0606073f5b3a34b2
# Parent  51867c8ad109ce33d2faec48af463d8907f3d1bc
tuned, following hints by IntelliJ IDEA;

diff -r 51867c8ad109 -r 74d6d09e1a36 src/Tools/jEdit/src/process_indicator.scala
--- a/src/Tools/jEdit/src/process_indicator.scala	Fri Aug 12 11:47:12 2022 +0200
+++ b/src/Tools/jEdit/src/process_indicator.scala	Fri Aug 12 11:47:41 2022 +0200
@@ -27,26 +27,24 @@
   private class Animation extends ImageIcon(passive_icon) {
     private var current_frame = 0
     private val timer =
-      new Timer(0, new ActionListener {
-        override def actionPerformed(e: ActionEvent): Unit = {
-          current_frame = (current_frame + 1) % active_icons.length
-          setImage(active_icons(current_frame))
-          label.repaint()
-        }
+      new Timer(0, { (_: ActionEvent) =>
+        current_frame = (current_frame + 1) % active_icons.length
+        setImage(active_icons(current_frame))
+        label.repaint()
       })
     timer.setRepeats(true)
 
     def update(rate: Int): Unit = {
       if (rate == 0) {
         setImage(passive_icon)
-        timer.stop
+        timer.stop()
         label.repaint()
       }
       else {
         val delay = 1000 / rate
         timer.setInitialDelay(delay)
         timer.setDelay(delay)
-        timer.restart
+        timer.restart()
       }
     }
   }