always invoke output: pending_output may be present due to other reasons;
authorwenzelm
Sun, 05 Mar 2017 18:59:39 +0100
changeset 65119 a7bedf94e71c
parent 65118 31fd8e41be02
child 65120 db6cc23fcf33
always invoke output: pending_output may be present due to other reasons;
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 =