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 _ => }