Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid empty tooltips;
authorwenzelm
Fri, 31 Aug 2012 15:24:26 +0200
changeset 49040 e5fc20c93e38
parent 49039 e780d1bf767e
child 49041 9edfd36a0355
avoid empty tooltips;
src/Tools/jEdit/src/isabelle_rendering.scala file | annotate | diff | comparison | revisions 
--- 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)))
   }
isabelle