`idris-quit` throws error when `*idris-proof-script*` buffer is present and `hs-minor-mode` activated

[keram]

hs-minor-mode Hideshow mode is a buffer-local minor mode that allows you to selectively display portions of a program, which are referred to as blocks.

It is not unusual to have it enabled globally in Emacs with: (add-hook 'prog-mode-hook 'hs-minor-mode)

But that leads to an error when trying to quit Idris as *idris-proof-script* mode also inherits from prog-mode. M-x idris-quit

Debugger entered--Lisp error: (error "Idris-Proof-Script Mode doesn’t support Hideshow M...")
  error("%s Mode doesn't support Hideshow Minor Mode" "Idris-Proof-Script")

It should be possible to disable the hs-minor-mode with: (add-hook 'idris-prover-script-mode-hook (lambda () (hs-minor-mode -1))) but it does not seem to be working for the idris-prover-script-mode

Options to consider:

• make the idris-prover-script-mode to support Hideshow mode (not probable)
• change parent mode for idris-prover-script-mode to other than prog-mode (maybe)
• disable hs-minor-mode internally for the mode so user doesn't have to do anything and the parent mode can stay prog-mode

[keram]

Closing in favour of added note to Readme file how to disable the hs-minor-mode https://github.com/idris-hackers/idris-mode#hideshow-minor-mode-hs-minor-mode In future we can revisit other options which do not require user intervention.