src/Tools/jEdit/src/pretty_tooltip.scala

       case _ =>
     }
   }
 
   def dismiss_descendant(parent: JComponent): Unit =
-    descendant(parent).foreach(dismiss(_))
+    descendant(parent).foreach(dismiss)
 
   def dismissed_all(): Boolean =
   {
     deactivate()
     if (stack.isEmpty) false

   }
 
 
   /* text area */
 
-  val pretty_text_area =
+  val pretty_text_area: Pretty_Text_Area =
     new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) {
       override def get_background() = Some(rendering.tooltip_color)
     }
 
   pretty_text_area.addFocusListener(new FocusAdapter {

           ((w_max - geometry.deco_width) / metric.unit).toInt) max 20
 
       val formatted = Pretty.formatted(info.info, margin = margin, metric = metric)
       val lines =
         XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)(
-          (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
+          (n: Int, s: String) => n + s.iterator.count(_ == '\n'))
 
       val h = painter.getLineHeight * lines + geometry.deco_height
       val margin1 =
         if (h <= h_max)
           (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })