Why:
The idris-list-holes-on-load was defined as interactive and as such, to be invokable by user but with nondeterministic behaviour affected by idris-hole-show-on-load.
Removing it in future will simplify the public api of idris-mode and reduce maintainance costs.
This commit also updates docs for idris-prover-success-hook and idris-load-file-success-hook to make explicit that they are also affected by the idris-hole-show-on-load variable.
Same time also moves their definition to idris-settings.el to make them easier to discover and connect the dots.
Why: The
idris-list-holes-on-loadwas defined as interactive and as such, to be invokable by user but with nondeterministic behaviour affected byidris-hole-show-on-load. Removing it in future will simplify the public api of idris-mode and reduce maintainance costs.This commit also updates docs for
idris-prover-success-hookandidris-load-file-success-hookto make explicit that they are also affected by theidris-hole-show-on-loadvariable. Same time also moves their definition toidris-settings.elto make them easier to discover and connect the dots.