src/Tools/VSCode/src/server.scala
changeset 64708 dd7f1a7e03f4
parent 64707 7157685b71e3
child 64709 5e6566ab78bf
--- a/src/Tools/VSCode/src/server.scala	Fri Dec 30 11:46:34 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Fri Dec 30 11:54:11 2016 +0100
@@ -125,7 +125,7 @@
   private val commands_changed =
     Session.Consumer[Session.Commands_Changed](getClass.getName) {
       case changed if changed.nodes.nonEmpty =>
-        resources.update_output(changed.nodes)
+        resources.update_output(changed.nodes.toList.map(_.node))
         delay_output.invoke()
       case _ =>
     }