(doc, distance)
| 7274 | // Sub-views need their line numbers shifted when text is added |
| 7275 | // above or below them in the parent document. |
| 7276 | function shiftDoc(doc, distance) { |
| 7277 | if (distance == 0) { |
| 7278 | return |
| 7279 | } |
| 7280 | doc.first += distance |
| 7281 | doc.sel = new Selection( |
| 7282 | map(doc.sel.ranges, function (range) { |
| 7283 | return new Range(Pos(range.anchor.line + distance, range.anchor.ch), Pos(range.head.line + distance, range.head.ch)) |
| 7284 | }), |
| 7285 | doc.sel.primIndex |
| 7286 | ) |
| 7287 | if (doc.cm) { |
| 7288 | regChange(doc.cm, doc.first, doc.first - distance, distance) |
| 7289 | for (var d = doc.cm.display, l = d.viewFrom; l < d.viewTo; l++) { |
| 7290 | regLineChange(doc.cm, l, "gutter") |
| 7291 | } |
| 7292 | } |
| 7293 | } |
| 7294 | |
| 7295 | // More lower-level change function, handling only a single document |
| 7296 | // (not linked ones). |
no test coverage detected