src/Tools/VSCode/extension/src/extension.ts
changeset 65233 e37209c0a42a
parent 65202 187277b77d50
child 65958 6338355b2a88
equal deleted inserted replaced
65232:ca571c8c0788 65233:e37209c0a42a
    62 
    62 
    63     /* decorations */
    63     /* decorations */
    64 
    64 
    65     decorations.init(context)
    65     decorations.init(context)
    66     vscode.workspace.onDidChangeConfiguration(() => decorations.init(context))
    66     vscode.workspace.onDidChangeConfiguration(() => decorations.init(context))
       
    67     vscode.workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document))
    67     vscode.window.onDidChangeActiveTextEditor(decorations.update_editor)
    68     vscode.window.onDidChangeActiveTextEditor(decorations.update_editor)
    68     vscode.workspace.onDidCloseTextDocument(decorations.close_document)
    69     vscode.workspace.onDidCloseTextDocument(decorations.close_document)
    69 
    70 
    70     client.onReady().then(() =>
    71     client.onReady().then(() =>
    71       client.onNotification(protocol.decoration_type, decorations.apply_decoration))
    72       client.onNotification(protocol.decoration_type, decorations.apply_decoration))