Configurable update for the server

imandra-ai / imandra-vscode

VSCode extension for developing imandra

Other

2 stars 0 forks source link

Closed ewenmaclean closed 3 years ago

ewenmaclean commented 3 years ago

Make settings in VSCode:

Imandra.Refresh on keystroke This setting states whether we refresh on every key stroke or only on a particular command (e.g. alt-r or something)
Show validated This setting sets whether the code is validated or not - i.e. whether to show green smileys(in lm)/highlighted code (in pm)