src/Tools/jEdit/src/jedit_rendering.scala
changeset 70079 990c6e8faf2c
parent 69666 c95edf19133b
child 70145 396e0120f7b8
     1.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 11 16:47:22 2019 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 11 18:58:06 2019 +0100
     1.3 @@ -291,7 +291,7 @@
     1.4    /* tooltips */
     1.5  
     1.6    def tooltip_margin: Int = options.int("jedit_tooltip_margin")
     1.7 -  def timing_threshold: Double = options.real("jedit_timing_threshold")
     1.8 +  override def timing_threshold: Double = options.real("jedit_timing_threshold")
     1.9  
    1.10    def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
    1.11      tooltips(Rendering.tooltip_elements, range).map(info => info.map(Pretty.fbreaks(_)))