lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

fix: periodically refresh semantic tokens

Open mhuisi opened this issue 11 months ago • 0 comments

This PR fixes an issue where the file worker would not provide the client with semantic tokens until the file had been elaborated completely. The file worker now also tells the client to refresh its semantic tokens after running "Restart File". This PR is based on #3271.

mhuisi avatar Mar 06 '24 14:03 mhuisi