# HG changeset patch
# User wenzelm
# Date 1348664151 -7200
# Node ID 0f087257ba046d95cbc6aebe9fc63055f3435a5c
# Parent 0d2f81eb7bf4d945ea9ecc2ef6011dbd263d086c
suppress empty tooltips;
diff -r 0d2f81eb7bf4 -r 0f087257ba04 src/Tools/Graphview/src/visualizer.scala
--- a/src/Tools/Graphview/src/visualizer.scala Wed Sep 26 14:52:18 2012 +0200
+++ b/src/Tools/Graphview/src/visualizer.scala Wed Sep 26 14:55:51 2012 +0200
@@ -144,12 +144,14 @@
object Tooltip {
def content(name: String): XML.Body = model.complete.get_node(name).content
- def text(name: String, fm: java.awt.FontMetrics): String =
+ def text(name: String, fm: java.awt.FontMetrics): String = // null
{
val txt = Pretty.string_of(content(name), 76, Pretty.font_metric(fm))
- "" + // FIXME proper scaling (!?)
- HTML.encode(txt) + "
"
+ if (txt == "") null
+ else
+ "" + // FIXME proper scaling (!?)
+ HTML.encode(txt) + "
"
}
}