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