| 1655 | } |
| 1656 | |
| 1657 | function findMarksAt(pos) { |
| 1658 | pos = clipPos(pos); |
| 1659 | var markers = [], marked = getLine(pos.line).marked; |
| 1660 | if (!marked) return markers; |
| 1661 | for (var i = 0, e = marked.length; i < e; ++i) { |
| 1662 | var m = marked[i]; |
| 1663 | if ((m.from == null || m.from <= pos.ch) && |
| 1664 | (m.to == null || m.to >= pos.ch)) |
| 1665 | markers.push(m.marker || m); |
| 1666 | } |
| 1667 | return markers; |
| 1668 | } |
| 1669 | |
| 1670 | function addGutterMarker(line, text, className) { |
| 1671 | if (typeof line == "number") line = getLine(clipLine(line)); |