search

banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
169 stars 39 forks source link

agda-mode supresses implicit markdown support from vscode #108

Open andreiburdusa opened 2 years ago

andreiburdusa commented 2 years ago

When the agda-mode extension is enabled, syntax highlighting and the "Open Preview" option (Ctrl+Shift+V) stop working for .lagda.md files.

banacorn commented 2 years ago

Which Markdown extension are you using? 👀

andreiburdusa commented 2 years ago

I'm not using any Markdown extension. This is how VS Code behaves when agda-mode is disabled: Screenshot from 2022-08-08 09-54-10 Screenshot from 2022-08-08 09-54-25 It has syntax highlighting and the "Open Preview" option for .lagda.md files.

And this is how it behaves when agda-mode is enabled: Screenshot from 2022-08-08 09-57-35 Screenshot from 2022-08-08 09-57-59 The syntax highlighting stops working and "Open Preview" option is not available anymore.