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