tuned signature;
authorwenzelm
Mon Mar 11 19:14:21 2019 +0100 (6 weeks ago ago)
changeset 7008027cf4287de43
parent 70079 990c6e8faf2c
child 70081 18a61caf5e68
tuned signature;
src/Pure/PIDE/rendering.scala
     1.1 --- a/src/Pure/PIDE/rendering.scala	Mon Mar 11 18:58:06 2019 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Mon Mar 11 19:14:21 2019 +0100
     1.3 @@ -519,7 +519,7 @@
     1.4  
     1.5    /* tooltips */
     1.6  
     1.7 -  def timing_threshold: Double
     1.8 +  def timing_threshold: Double = 0.0
     1.9  
    1.10    private sealed case class Tooltip_Info(
    1.11      range: Text.Range,