| 1455 | } |
| 1456 | |
| 1457 | function findMarksAt(pos) { |
| 1458 | pos = clipPos(pos); |
| 1459 | var markers = [], marked = getLine(pos.line).marked; |
| 1460 | if (!marked) return markers; |
| 1461 | for (var i = 0, e = marked.length; i < e; ++i) { |
| 1462 | var m = marked[i]; |
| 1463 | if ((m.from == null || m.from <= pos.ch) && |
| 1464 | (m.to == null || m.to >= pos.ch)) |
| 1465 | markers.push(m.marker || m); |
| 1466 | } |
| 1467 | return markers; |
| 1468 | } |
| 1469 | |
| 1470 | function addGutterMarker(line, text, className) { |
| 1471 | if (typeof line == "number") line = getLine(clipLine(line)); |