remove unnecessary load step for some commands?

[swr1bm86]

currently, it will type check file before every command like here. and type checking is really time-costing that we have to wait for almost 10 seconds if only want to get the definition of an identifier or just want to create a case template. so do we really need to load file before every command? i can see the advantage of it, but it is just not so efficient for programming with Idris.

@melted @david-christiansen @archaeron

[david-christiansen]

The Emacs mode is selective about type checking. It only happens if the file has been modified since the last type check, and it only does it at all for commands that do editing, where they only make sense for type-checked code. This has worked pretty well. There's also support for only loading part of the file, which the "dirty bit" tracking also supports.

On September 12, 2016 12:29:53 PM GMT+09:00, "(λ _ λ)" [email protected] wrote:

currently, it will type check file before every command like here. and type checking is really time-costing that we have to wait for almost 10 seconds if only want to get the definition of an identifier or just want to create a case template. so do we really need to load file before every command? i can see the advantage of it, but it is just not so efficient for programming with Idris.

@melted @david-christiansen @archaeron

[swr1bm86]

@david-christiansen thx! your answer inspired me a lot! i think the first way you mentioned is easy to be implemented for vscode extension since there is a version property for the document instance, and i will try to find how to wrap it up for atom :)