(spans, span)
| 6320 | // Remove a span from an array, returning undefined if no spans are |
| 6321 | // left (we don't store arrays for lines without spans). |
| 6322 | function removeMarkedSpan(spans, span) { |
| 6323 | for (var r, i = 0; i < spans.length; ++i) |
| 6324 | if (spans[i] != span) (r || (r = [])).push(spans[i]); |
| 6325 | return r; |
| 6326 | } |
| 6327 | // Add a span to a line. |
| 6328 | function addMarkedSpan(line, span) { |
| 6329 | line.markedSpans = line.markedSpans ? line.markedSpans.concat([span]) : [span]; |