# HG changeset patch
# User wenzelm
# Date 1488736779 -3600
# Node ID a7bedf94e71cf2e85d64c48b2bbccad437c3fa76
# Parent  31fd8e41be02367a20d041d3e7653c5ec873b2a2
always invoke output: pending_output may be present due to other reasons;

diff -r 31fd8e41be02 -r a7bedf94e71c src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Sun Mar 05 18:58:17 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sun Mar 05 18:59:39 2017 +0100
@@ -161,10 +161,9 @@
 
   private val prover_output =
     Session.Consumer[Session.Commands_Changed](getClass.getName) {
-      case changed if changed.nodes.nonEmpty =>
+      case changed =>
         resources.update_output(changed.nodes.toList.map(resources.node_file(_)))
         delay_output.invoke()
-      case _ =>
     }
 
   private val syslog =