Support github.dev & vscode.dev web editors
lemmy opened this issue · 2 comments
The extension doesn't work in the github.dev web editor: "The 'TLA+' extension is not available in Visual Studio Code for the Web."
Why is an extension not installable in the browser#
There are a small number of extensions that have built-in assumptions or need to run on the desktop. Examples are when an extension accesses files from the VS Code installation on the desktop or when an extension depends on an executable that must run in a desktop environment. When you try to install such an extension in the browser, you will be informed that the extension is not available.
Notice such an extension can still be used when connecting to a Codespace from VS Code running on the desktop.
(from https://code.visualstudio.com/docs/remote/codespaces#_why-is-an-extension-not-installable-in-the-browser) Also, https://code.visualstudio.com/updates/v1_60#_web-extensions has technical background.
It is unlikely that TLC will ever run in the browser, but syntax highlighting should be possible.
Likely related to make web-views work: https://code.visualstudio.com/blogs/2021/10/11/webview-ui-toolkit
Running SANY in WASM could probably be accomplished by using GraalVM: https://www.graalvm.org/
A more promising approach would be to use @will62794 https://github.com/will62794/tla-web for the purely browser-based variant of the VSCode extension.