# HG changeset patch
# User wenzelm
# Date 1502357739 -7200
# Node ID fa473c07d86c5f00148a765f89dd6e2be94e9f3e
# Parent  8e614c2230007d4abbf9aae727b5836e623f0899
tuned;

diff -r 8e614c223000 -r fa473c07d86c src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Wed Aug 09 23:41:47 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Thu Aug 10 11:35:39 2017 +0200
@@ -232,11 +232,9 @@
         update_output(changed.nodes.toList.map(resources.node_file(_)))
     }
 
-  private val syslog =
-    Session.Consumer[Prover.Message](getClass.getName) {
-      case output: Prover.Output if output.is_syslog =>
-        channel.log_writeln(resources.output_xml(output.message))
-      case _ =>
+  private val syslog_messages =
+    Session.Consumer[Prover.Output](getClass.getName) {
+      case output => channel.log_writeln(resources.output_xml(output.message))
     }
 
 
@@ -288,7 +286,7 @@
       session_.change(_ => Some(session))
 
       session.commands_changed += prover_output
-      session.all_messages += syslog
+      session.syslog_messages += syslog_messages
 
       dynamic_output.init()
 
@@ -317,7 +315,7 @@
     session_.change({
       case Some(session) =>
         session.commands_changed -= prover_output
-        session.all_messages -= syslog
+        session.syslog_messages -= syslog_messages
 
         dynamic_output.exit()