equal
deleted
inserted
replaced
190 const document = document_decorations.get(uri.toString()) || new Map<string, Content>() |
190 const document = document_decorations.get(uri.toString()) || new Map<string, Content>() |
191 document.set(decoration.type, content) |
191 document.set(decoration.type, content) |
192 document_decorations.set(uri.toString(), document) |
192 document_decorations.set(uri.toString(), document) |
193 |
193 |
194 for (const editor of window.visibleTextEditors) { |
194 for (const editor of window.visibleTextEditors) { |
195 if (uri.toString === editor.document.uri.toString) { |
195 if (uri.toString() === editor.document.uri.toString()) { |
196 editor.setDecorations(typ, content) |
196 editor.setDecorations(typ, content) |
197 } |
197 } |
198 } |
198 } |
199 } |
199 } |
200 } |
200 } |