agda-mode-vscode icon indicating copy to clipboard operation
agda-mode-vscode copied to clipboard

support history for normalisation field

Open bblfish opened this issue 5 years ago • 1 comments

I think emacs allows one to use the up and down arrows for the normalisation field, to scroll through the history of previous normalisations. It would be useful to be able to do the same thing in vscode.

Other bugs:

  • going back in vscode with the arrow after having made a mistake, allows one only to type one character. The cursor then immediately moves to the right, so that one has to reposition the cursor back to where it was
  • I don't think it would harm to have a much longer field to enter a normalisation statement. Currently it is quite small.

bblfish avatar Nov 06 '20 13:11 bblfish

Thanks for the feedback, I'll break them into 3 different issues.

banacorn avatar Nov 08 '20 08:11 banacorn