| 108 | // ============================================================================ |
| 109 | |
| 110 | function buildDecos(hints: ProcessedHint[], docLen: number): DecorationSet { |
| 111 | if (!hints.length) return Decoration.none; |
| 112 | |
| 113 | const decos: Range<Decoration>[] = []; |
| 114 | for (const h of hints) { |
| 115 | if (h.pos < 0 || h.pos > docLen) continue; |
| 116 | decos.push( |
| 117 | Decoration.widget({ |
| 118 | widget: new HintWidget( |
| 119 | h.label, |
| 120 | h.paddingLeft ?? false, |
| 121 | h.paddingRight ?? false, |
| 122 | h.tooltip, |
| 123 | ), |
| 124 | side: 1, |
| 125 | }).range(h.pos), |
| 126 | ); |
| 127 | } |
| 128 | return RangeSet.of(decos, true); |
| 129 | } |
| 130 | |
| 131 | // ============================================================================ |
| 132 | // Plugin |