| author | wenzelm | 
| Tue, 17 Oct 2023 18:55:29 +0200 | |
| changeset 78792 | 103467dc5117 | 
| parent 75126 | da1108a6d249 | 
| child 81035 | 56594fac1dab | 
| permissions | -rw-r--r-- | 
| 
75126
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
1  | 
(function () {
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
2  | 
const vscode = acquireVsCodeApi();  | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
3  | 
|
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
4  | 
    for (const link of document.querySelectorAll('a[href^="file:"]')) {
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
5  | 
        link.addEventListener('click', () => {
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
6  | 
            vscode.postMessage({
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
7  | 
command: "open",  | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
8  | 
                link: link.getAttribute('href'),
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
9  | 
});  | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
10  | 
});  | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
11  | 
}  | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
12  | 
|
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
13  | 
    const auto_update = document.getElementById('auto_update');
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
14  | 
    auto_update && auto_update.addEventListener('change', (e) => {
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
15  | 
            vscode.postMessage({'command': 'auto_update', 'enabled': e.target.checked}) ;
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
16  | 
});  | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
17  | 
|
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
18  | 
    const update_button = document.getElementById('update_button');
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
19  | 
    update_button && update_button.addEventListener('click', (e) => {
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
20  | 
            vscode.postMessage({'command': 'update'}) 
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
21  | 
});  | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
22  | 
|
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
23  | 
    const locate_button = document.getElementById('locate_button');
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
24  | 
    locate_button && locate_button.addEventListener('click', (e) => {
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
25  | 
            vscode.postMessage({'command': 'locate'});
 | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
26  | 
});  | 
| 
 
da1108a6d249
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
 
wenzelm 
parents:  
diff
changeset
 | 
27  | 
}());  |