# HG changeset patch
# User wenzelm
# Date 1517348760 -3600
# Node ID 2b30e03a722974eb212eb851ba308e3f6f49c2fc
# Parent  26a6af52f1f93c3025e96b0210503544855f627e
clarified lines: like split_lines;

diff -r 26a6af52f1f9 -r 2b30e03a7229 src/Tools/jEdit/src/pretty_tooltip.scala
--- 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) })