zjhmale / vscode-idris

Idris for Visual Studio Code
https://marketplace.visualstudio.com/items?itemName=zjhmale.Idris
BSD 3-Clause "New" or "Revised" License
106 stars 21 forks source link

After type checking error ("didn't load"), hovering messages becomes confusing #133

Closed raptazure closed 3 years ago

raptazure commented 3 years ago

Thanks for this great extension! But I found something related to error message presentation can be improved. If there are some errors after type checking, the error message can't be presented properly. Instead, "didn't load" warning message keeps popping up. And hovering on anything now will show the error message, which nearly breaks the hover functionality, like this. image I wonder if we can show the error message in the output session without influencing hovering on unrelated things. it will offer better user experience, I think.