search

banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
169 stars 39 forks source link

Feature request: Toggle display of irrelevant arguments #72

Closed isti115 closed 2 years ago

isti115 commented 2 years ago

First of all thank you for your great work! I have been teaching at university using proof assistants such as Coq and Agda for multiple years now and getting the students to properly set up and use Emacs always took lots of time and effort and now thanks to this plugin I can suggest VSCode for them, which most of them already know, use and like.

What I'd like to request from you is the addition of the option to toggle the display of irrelevant arguments (C-c C-x C-i). I guess that this shouldn't be too hard to implement, since you already provide the option to toggle the display of hidden arguments. In case you don't have time to allocate for this issue currently, I might try creating a pull request. (I have never developed VSCode extensions before myself [and haven't written ReScript either], but I hope that I just need to duplicate and modify some parts for this to work.)

banacorn commented 2 years ago

Thanks! This shouldn't take too long!