idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
267 stars 70 forks source link

Jump back to buffer from which we came to Idris buffer #557

Closed keram closed 1 year ago

keram commented 1 year ago

With current version, when Idris buffer is displayed in window that already contains other buffer then on pressing "q" to quit Idris buffer the focus stay in the window of the Idris buffer.

This change ensures that the focus returns to the buffer and window from where we came to the Idris buffer.

Inspired by the work in idris-community/idris2-mode for Info buffer https://github.com/idris-community/idris2-mode/blob/0f7c496c8fb9df9c05958f30e5633569a9b9e3a7/idris2-info.el

Before:

https://user-images.githubusercontent.com/578608/200193859-33014c29-e6f9-4d30-9129-5ca24e8671dc.mp4

After:

https://user-images.githubusercontent.com/578608/200193868-e0de738f-ef81-454f-986a-56dbf22b45f8.mp4

Relates to https://github.com/idris-hackers/idris-mode/pull/556

keram commented 1 year ago

Having an error when trying to run make

idris-commands.el:276:17: Error: assignment to free variable ‘idris-buffer-to-return-to-from-idris-buffer’

so may consider to change the approach to same as in https://github.com/idris-hackers/idris-mode/pull/558/files#diff-57c9b17a4d33ee59f640d96a562f576b22d600b5adb02038a989e8eb1d2e76c5R956-R959

jfdm commented 1 year ago

This PR now has some conflicts, if you can sort them out I will look to merge this when I am next free. Thanks.

keram commented 1 year ago

Yes, this conflict is expected I can sort it out later as i did that already on my local machine.

keram commented 1 year ago

Note for myself: Tests on Mac M1 are flaky. Having only Idris2 installed running make test result in:

...
Test idris-test-idris-quit-logging-enabled condition:                                                                                                                                   
    (file-missing "Searching for program" "No such file or directory" "idris")                                                                                                          
   FAILED  6/9  idris-test-idris-quit-logging-enabled (0.000644 sec)                        
   passed  7/9  idris-test-ipkg-packages-with-underscores-and-dashes (0.014320 sec)                                                                                                     
Directory ‘~/.emacs.d/vendor/idris-mode/test-data/test-data/test-data/’ does not exist; create? (y or n) n  

make test2 hangs on:

Idris disconnected: deleted
Idris disconnected: killed: 9
   passed  1/8  idris-test2-error-buffer (4.245946 sec)
   passed  2/8  idris-test2-find-cmdline-args (0.052587 sec)
Connected. Marek, this could be the start of a beautiful proof.
Preparing compiler note tree...

make test3 passes 🟢

jfdm commented 1 year ago

At somepoint we should make the test-harness more 'robust'.

Thanks for the contributions!