search

banacorn / agda-mode

agda-mode on Atom
https://atom.io/packages/agda-mode
MIT License
58 stars 14 forks source link

Tab focus in Atom when computing normal form / inferring type #104

Closed pnlph closed 5 years ago

pnlph commented 5 years ago

Description

When loading C-c C-l a file and then trying to compute a normal form C-c C-n the focus of the cursor in Atom stays in the tab of the agda file.

The same is the case for inferring a type C-c C-d.

This forces the user to manually change the focus in Atom by clicking the field in the Agda mode tab.

Expected behavior

When the user tries to perform any computation in the agda mode, the focus should also be changed to that tab and the cursor position placed in the field. Like this, the user can write or paste right away.

After the computation it behaves OK, being focus correctly changed to the corresponding agda file tab.

banacorn commented 5 years ago

Fixed! Thank you for reporting this!