# HG changeset patch
# User wenzelm
# Date 1346419466 -7200
# Node ID e5fc20c93e38722883762b82c52c88ed6fdbc957
# Parent  e780d1bf767e4dc831a31da069a5da8b1ecd6bf3
avoid empty tooltips;

diff -r e780d1bf767e -r e5fc20c93e38 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 31 15:03:44 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 31 15:24:26 2012 +0200
@@ -166,8 +166,8 @@
               markup == Isabelle_Markup.WARNING ||
               markup == Isabelle_Markup.ERROR =>
             msgs + (serial -> tooltip_text(msg))
-          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
-            msgs + (Document.new_id() -> tooltip_text(msg))
+          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), body)))
+          if !body.isEmpty => msgs + (Document.new_id() -> tooltip_text(msg))
         }).toList.flatMap(_.info)
     if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
   }