src/Pure/PIDE/rendering.scala
changeset 65107 70b0113fa4ef
parent 65104 66b19d05dcee
child 65121 12c6774a8f65
     1.1 --- a/src/Pure/PIDE/rendering.scala	Sat Mar 04 21:04:44 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Sat Mar 04 21:47:26 2017 +0100
     1.3 @@ -134,7 +134,6 @@
     1.4  
     1.5    /* tooltips */
     1.6  
     1.7 -  def tooltip_margin: Int
     1.8    def timing_threshold: Double
     1.9  
    1.10    def tooltips(range: Text.Range): Option[Text.Info[List[XML.Tree]]] =