(doc, distance)
| 4462 | // Sub-views need their line numbers shifted when text is added |
| 4463 | // above or below them in the parent document. |
| 4464 | function shiftDoc(doc, distance) { |
| 4465 | if (distance == 0) return; |
| 4466 | doc.first += distance; |
| 4467 | doc.sel = new Selection(map(doc.sel.ranges, function(range) { |
| 4468 | return new Range(Pos(range.anchor.line + distance, range.anchor.ch), |
| 4469 | Pos(range.head.line + distance, range.head.ch)); |
| 4470 | }), doc.sel.primIndex); |
| 4471 | if (doc.cm) { |
| 4472 | regChange(doc.cm, doc.first, doc.first - distance, distance); |
| 4473 | for (var d = doc.cm.display, l = d.viewFrom; l < d.viewTo; l++) |
| 4474 | regLineChange(doc.cm, l, "gutter"); |
| 4475 | } |
| 4476 | } |
| 4477 | |
| 4478 | // More lower-level change function, handling only a single document |
| 4479 | // (not linked ones). |
no test coverage detected