equal
deleted
inserted
replaced
218 } |
218 } |
219 |
219 |
220 |
220 |
221 /* pending output */ |
221 /* pending output */ |
222 |
222 |
223 def update_output(changed_nodes: List[JFile]): Unit = |
223 def update_output(changed_nodes: Traversable[JFile]): Unit = |
224 state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes)) |
224 state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes)) |
225 |
225 |
226 def flush_output(channel: Channel) |
226 def flush_output(channel: Channel) |
227 { |
227 { |
228 state.change(st => |
228 state.change(st => |