suppress empty results;
authorwenzelm
Thu Jan 05 16:16:18 2017 +0100 (2017-01-05 ago)
changeset 64802adc4c84b692c
parent 64801 5ecc426922b7
child 64803 27328dcaf64c
suppress empty results;
src/Pure/PIDE/command.scala
src/Tools/VSCode/src/vscode_rendering.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Jan 05 15:32:32 2017 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Jan 05 16:16:18 2017 +0100
     1.3 @@ -36,6 +36,7 @@
     1.4  
     1.5    final class Results private(private val rep: SortedMap[Long, XML.Tree])
     1.6    {
     1.7 +    def is_empty: Boolean = rep.isEmpty
     1.8      def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
     1.9      def get(serial: Long): Option[XML.Tree] = rep.get(serial)
    1.10      def iterator: Iterator[Results.Entry] = rep.iterator
     2.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Thu Jan 05 15:32:32 2017 +0100
     2.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Thu Jan 05 16:16:18 2017 +0100
     2.3 @@ -53,7 +53,7 @@
     2.4          if body.nonEmpty => Some(res + (i -> msg))
     2.5  
     2.6          case _ => None
     2.7 -      })
     2.8 +      }).filterNot(info => info.info.is_empty)
     2.9  
    2.10    val diagnostics_margin = options.int("vscode_diagnostics_margin")
    2.11