src/Tools/VSCode/extension/media/main.js
author Fabian Huch <huch@in.tum.de>
Fri, 08 Dec 2023 17:00:13 +0100
changeset 79191 ee405c40db72
parent 75126 da1108a6d249
child 81035 56594fac1dab
permissions -rw-r--r--
store previous build jobs in graph so schedules can be used later in the build process;

(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'});
        });
}());