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

Customize highlighting levels #119

Open plt-amy opened 2 years ago

plt-amy commented 2 years ago

The code already supports generating IOTCM ... strings with different highlighting levels:

https://github.com/banacorn/agda-mode-vscode/blob/c9c24654d2bdbfca7ce9a7bdbf4b8c63f1a9df87/src/Request.res#L91-L98

but they're always called with NonInteractive:

https://github.com/banacorn/agda-mode-vscode/blob/c9c24654d2bdbfca7ce9a7bdbf4b8c63f1a9df87/src/Request.res#L105-L109

Could there be a setting to change this?