# HG changeset patch
# User wenzelm
# Date 1483629378 -3600
# Node ID adc4c84b692c7c9b330ca3277ac8ae9f94603c8c
# Parent  5ecc426922b79abb755c7329272e1523e8032b6c
suppress empty results;

diff -r 5ecc426922b7 -r adc4c84b692c src/Pure/PIDE/command.scala
--- 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
diff -r 5ecc426922b7 -r adc4c84b692c src/Tools/VSCode/src/vscode_rendering.scala
--- 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")