--- a/src/Tools/jEdit/src/pretty_tooltip.scala Tue Jan 30 22:46:00 2018 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Tue Jan 30 23:01:38 2018 +0100
@@ -259,7 +259,7 @@
((rendering.tooltip_margin * metric.average) min
((w_max - geometry.deco_width) / metric.unit).toInt) max 20
- val formatted = Pretty.formatted(info.info, margin, metric)
+ 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)