Why:
To reduce steps to show holes for current buffer.
Currently when idris file buffer is open and user tries:
M-x idris-list-holes he gets error:
"Buffer *.idr has no process"
If there is a running idris process but other file was loaded,
the result may be that holes for the previous buffer
or message "No holes found!" is displayed.
Why: To reduce steps to show holes for current buffer. Currently when idris file buffer is open and user tries:
M-x idris-list-holeshe gets error: "Buffer *.idr has no process"If there is a running idris process but other file was loaded, the result may be that holes for the previous buffer or message "No holes found!" is displayed.