search

banacorn / agda-mode

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

Menu options #60

Closed jonaprieto closed 6 years ago

jonaprieto commented 6 years ago

Is there any chance to put the following menu:

image

In the options of the menu (right-click on the mouse)? image

That will be very useful for some options!

banacorn commented 6 years ago

Yes! seems like it's totally doable: https://atom.io/docs/api/v0.188.0/ContextMenuManager.

I hope there's some way for a user to decide which command to be listed in the menu, because as you can see, there are quite a lot of them.

jonaprieto commented 6 years ago

I might be wrong, I don't remember exactly how that's in emacs, but I have the impression that emacs shows all the options.

banacorn commented 6 years ago

It turned out that having to many commands is not a problem, just cram them in our own sub-menu.

image

jonaprieto commented 6 years ago

With the last release 0.7.14 I have nothing

banacorn commented 6 years ago

Silly me, I forgot to merge the developing branch. 😂

jonaprieto commented 6 years ago

It works now, thanks a lot