This isn't going to fix this issue, but it will stop sending extra pointless requests to the IDE process.
If you call document.getWordRangeAtPosition(position) when the position is a space between words, it returns null. And if you call document.getText(null), you get the whole document. If you send the whole document to Idris, it doesn't return a type, but it's quite heavy for a meaningless action.
This isn't going to fix this issue, but it will stop sending extra pointless requests to the IDE process.
If you call
document.getWordRangeAtPosition(position)when the position is a space between words, it returns null. And if you calldocument.getText(null), you get the whole document. If you send the whole document to Idris, it doesn't return a type, but it's quite heavy for a meaningless action.