(left, top, width, bottom)
| 825 | var padding = paddingH(cm.display), leftSide = padding.left, rightSide = display.lineSpace.offsetWidth - padding.right; |
| 826 | |
| 827 | function add(left, top, width, bottom) { |
| 828 | if (top < 0) top = 0; |
| 829 | fragment.appendChild(elt("div", null, "CodeMirror-selected", "position: absolute; left: " + left + |
| 830 | "px; top: " + top + "px; width: " + (width == null ? rightSide - left : width) + |
| 831 | "px; height: " + (bottom - top) + "px")); |
| 832 | } |
| 833 | |
| 834 | function drawForLine(line, fromArg, toArg) { |
| 835 | var lineObj = getLine(doc, line); |
no test coverage detected