Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

The web extension does not export any API #877

Open
amblafont opened this issue Dec 1, 2024 · 0 comments
Open

The web extension does not export any API #877

amblafont opened this issue Dec 1, 2024 · 0 comments

Comments

@amblafont
Copy link
Contributor

Describe the bug

extensions.getExtension('ejgallego.coq-lsp').exports is undefined when coq-lsp is running on vscode.dev.

To Reproduce
Try the above line in a new vscode web extension, with coq-lsp already installed. To test the new web extension, I used the @vscode/test-web method documented here: https://code.visualstudio.com/api/extension-guides/web-extensions#test-your-web-extension.

Expected behavior
I expect this line to return an object of type CoqLspAPI (as it does when the extension is running on desktop)

Desktop (please complete the following information):

  • coq-lsp version 0.2.2
  • VS Code version 1.95.3

Additional context

I would like to reimplement Coreact-yade as a web extension exploiting the new features of coq-lsp (full implementation of coq running in vscode.dev)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants