agda-mode-vscode icon indicating copy to clipboard operation
agda-mode-vscode copied to clipboard

Published 20 hours ago • verified publisher icon banacorn

option for automatic loading of Agda files?

Open bblfish opened this issue 3 years ago • 1 comments

In emacs loading an Agda file from an already loaded file reached by clicking on link loads the reached file. That is actually quite nice when exploring code. I find myself in vscode always typing ^-C ^-L . Is this not enabled because of risks of memory usage being high?

bblfish avatar Jan 02 '21 16:01 bblfish

I think we can have it enabled by default (like in Emacs), and have an option in the settings for disabling it.

banacorn avatar Jan 04 '21 08:01 banacorn