clarified lines: like split_lines;

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Jan 30 20:36:18 2018 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Jan 30 22:46:00 2018 +0100
@@ -261,10 +261,10 @@
 
       val formatted = Pretty.formatted(info.info, margin, metric)
       val lines =
-        XML.traverse_text(formatted)(0)(
+        XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)(
           (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
 
-      val h = painter.getLineHeight * (lines + 1) + geometry.deco_height
+      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) })