(left, top, width, bottom)
| 2242 | var rightSide = Math.max(display.sizerWidth, displayWidth(cm) - display.sizer.offsetLeft) - padding.right; |
| 2243 | |
| 2244 | function add(left, top, width, bottom) { |
| 2245 | if (top < 0) top = 0; |
| 2246 | top = Math.round(top); |
| 2247 | bottom = Math.round(bottom); |
| 2248 | fragment.appendChild(elt("div", null, "CodeMirror-selected", "position: absolute; left: " + left + |
| 2249 | "px; top: " + top + "px; width: " + (width == null ? rightSide - left : width) + |
| 2250 | "px; height: " + (bottom - top) + "px")); |
| 2251 | } |
| 2252 | |
| 2253 | function drawForLine(line, fromArg, toArg) { |
| 2254 | var lineObj = getLine(doc, line); |
no test coverage detected