src/Tools/VSCode/extension/media/main.js
author wenzelm
Mon, 11 Sep 2023 19:30:48 +0200
changeset 78659 b5f3d1051b13
parent 75126 da1108a6d249
child 81035 56594fac1dab
permissions -rw-r--r--
tuned;

(function () {
    const vscode = acquireVsCodeApi();
        
    for (const link of document.querySelectorAll('a[href^="file:"]')) {
        link.addEventListener('click', () => {
            vscode.postMessage({
                command: "open",
                link: link.getAttribute('href'),
            });
        });
    }
    
    const auto_update = document.getElementById('auto_update');
    auto_update && auto_update.addEventListener('change', (e) => {
            vscode.postMessage({'command': 'auto_update', 'enabled': e.target.checked}) ;
        });

    const update_button = document.getElementById('update_button');
    update_button && update_button.addEventListener('click', (e) => {
            vscode.postMessage({'command': 'update'}) 
        });
        
    const locate_button = document.getElementById('locate_button');
    locate_button && locate_button.addEventListener('click', (e) => {
            vscode.postMessage({'command': 'locate'});
        });
}());