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))