src/Tools/jEdit/src/rich_text_area.scala

                   else rendering.tooltip_message(range)
                 if (!tip.isEmpty) {
                   val painter = text_area.getPainter
                   val y1 = y + painter.getFontMetrics.getHeight / 2
                   val results = rendering.command_results(range)
-                  new Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
+                  Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
                 }
             }
           }
           tooltip_event = None
         case _ =>