(left, top, width, bottom)
| 2353 | var rightSide = Math.max(display.sizerWidth, displayWidth(cm) - display.sizer.offsetLeft) - padding.right; |
| 2354 | |
| 2355 | function add(left, top, width, bottom) { |
| 2356 | if (top < 0) top = 0; |
| 2357 | top = Math.round(top); |
| 2358 | bottom = Math.round(bottom); |
| 2359 | fragment.appendChild(elt("div", null, "CodeMirror-selected", "position: absolute; left: " + left + |
| 2360 | "px; top: " + top + "px; width: " + (width == null ? rightSide - left : width) + |
| 2361 | "px; height: " + (bottom - top) + "px")); |
| 2362 | } |
| 2363 | |
| 2364 | function drawForLine(line, fromArg, toArg) { |
| 2365 | var lineObj = getLine(doc, line); |
no test coverage detected