--- a/src/Pure/PIDE/rendering.scala Sat Mar 04 21:04:44 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala Sat Mar 04 21:47:26 2017 +0100
@@ -134,7 +134,6 @@
/* tooltips */
- def tooltip_margin: Int
def timing_threshold: Double
def tooltips(range: Text.Range): Option[Text.Info[List[XML.Tree]]] =