equal
deleted
inserted
replaced
123 /* output to client */ |
123 /* output to client */ |
124 |
124 |
125 private val commands_changed = |
125 private val commands_changed = |
126 Session.Consumer[Session.Commands_Changed](getClass.getName) { |
126 Session.Consumer[Session.Commands_Changed](getClass.getName) { |
127 case changed if changed.nodes.nonEmpty => |
127 case changed if changed.nodes.nonEmpty => |
128 resources.update_output(changed.nodes) |
128 resources.update_output(changed.nodes.toList.map(_.node)) |
129 delay_output.invoke() |
129 delay_output.invoke() |
130 case _ => |
130 case _ => |
131 } |
131 } |
132 |
132 |
133 private val delay_output: Standard_Thread.Delay = |
133 private val delay_output: Standard_Thread.Delay = |