# HG changeset patch
# User wenzelm
# Date 1552328061 -3600
# Node ID 27cf4287de43cc0112be6e664e94ba0c2a16da01
# Parent  990c6e8faf2cfdd6bbc3bd1d8abdd4c0110de529
tuned signature;

diff -r 990c6e8faf2c -r 27cf4287de43 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Mar 11 18:58:06 2019 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Mar 11 19:14:21 2019 +0100
@@ -519,7 +519,7 @@
 
   /* tooltips */
 
-  def timing_threshold: Double
+  def timing_threshold: Double = 0.0
 
   private sealed case class Tooltip_Info(
     range: Text.Range,