# HG changeset patch
# User wenzelm
# Date 1735213105 -3600
# Node ID 4268b8f841e458107769934eb313d69dca1659ef
# Parent  36c5eabd62ec0b2ec0c984218e4ffdf9a0ad5ed1
tuned: fewer warnings in IntelliJ IDEA;

diff -r 36c5eabd62ec -r 4268b8f841e4 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Thu Dec 26 12:08:05 2024 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Thu Dec 26 12:38:25 2024 +0100
@@ -133,8 +133,7 @@
         handle_update()
     }
     tooltip = threshold_tooltip
-    verifier = ((s: String) =>
-      s match { case Value.Double(x) => x >= 0.0 case _ => false })
+    verifier = { case Value.Double(x) => x >= 0.0 case _ => false }
   }
 
   private val controls = Wrap_Panel(List(threshold_label, threshold_value))