src/Tools/jEdit/src/utils/Delay.scala

--- a/src/Tools/jEdit/src/utils/Delay.scala	Tue Jan 27 18:58:16 2009 +0100
+++ b/src/Tools/jEdit/src/utils/Delay.scala	Tue Jan 27 19:27:59 2009 +0100
@@ -12,14 +12,14 @@
 class Delay(amount : Int, action : () => Unit) {
 
   val timer : Timer = new Timer(amount, new ActionListener {
-      override def actionPerformed(e:ActionEvent){
-        action ()
+      override def actionPerformed(e:ActionEvent) {
+        action()
       }
     })
   // if called very often, action is executed at most once
   // in amount milliseconds
-  def delay_or_ignore () = {
-    if (! timer.isRunning()){
+  def delay_or_ignore() = {
+    if (!timer.isRunning()) {
       timer.setRepeats(false)
       timer.start()
     }