suppress empty results;

--- a/src/Pure/PIDE/command.scala	Thu Jan 05 15:32:32 2017 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Jan 05 16:16:18 2017 +0100
@@ -36,6 +36,7 @@
 
   final class Results private(private val rep: SortedMap[Long, XML.Tree])
   {
+    def is_empty: Boolean = rep.isEmpty
     def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
     def get(serial: Long): Option[XML.Tree] = rep.get(serial)
     def iterator: Iterator[Results.Entry] = rep.iterator

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Thu Jan 05 15:32:32 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Thu Jan 05 16:16:18 2017 +0100
@@ -53,7 +53,7 @@
         if body.nonEmpty => Some(res + (i -> msg))
 
         case _ => None
-      })
+      }).filterNot(info => info.info.is_empty)
 
   val diagnostics_margin = options.int("vscode_diagnostics_margin")