(h: Highlight)
| 756 | } |
| 757 | |
| 758 | function dimContent(h: Highlight): void { |
| 759 | for (const line of h.lines) { |
| 760 | if (line.length > 0) { |
| 761 | line[0]![1] = DIM + line[0]![1] |
| 762 | const last = line.length - 1 |
| 763 | line[last]![1] = line[last]![1] + UNDIM |
| 764 | } |
| 765 | } |
| 766 | } |
| 767 | |
| 768 | function applyBackground(h: Highlight, theme: Theme, ranges: Range[]): void { |
| 769 | if (!h.marker) return |