Coq: make printing parentheses flag accessible

[hendriktews]

Add menu entry and Coq keymap binding available to set/unset the Printing Parentheses flag.

[hendriktews]

I would have preferred C-c C-a C-( and C-c C-a C-) as keybinding, but those keys are already taken. On the other hand C-9 is much easier to type than C-(, of course accepting the discrimination of (at least) the German keyboard users (where the parentheses are on 8 and 9 ;-).

[hendriktews]

@sertel: Is this (part of) what you were missing in PG?

[sertel]

Yes, but also for toggling the Printing Notations flag.

[hendriktews]

Are you fine with a menu entry only? Otherwise, do you have a suggestion for a keybinding with the C-c C-a prefix? (Already taken are: C-a, C-b, C-c, TAB, C-l, RET, C-n, C-o, C-p, C-q, C-r, C-s, C-t, C-w, !, [, g, h, r, t, C-SPC, C-(, C-), C-0, C-9, C-<return>).

[hendriktews]

Now with notations. I defined n and N as keybindings, because C-n is already taken for locate notation.

[hendriktews]

@sertel : depending on your desperation level you may pick this change. Think twice before you switch to this branch, because it contains the currently not yet fixed #781.

[Matafou]

On this feature: there is already a way to send a command to Coq enclosed inside a Set Printing All / Unset Printing All. I find it more useful than a toggle. We could think of extending this to other enclosing flags?

If you don't know this feature try to hit C-u before your usual shortcut for Print or About or Show.

Example:

Lemma foo: forall n:nat, n = n.
Proof.

then hit C-u C-c C-a C-s RET.

[Matafou]

sorry had to edit the shortcut at the end.

[hendriktews]

OK, didn't know that. I saw the other toggles for implicit, coercions, and so on, and thought parenthesis and notations were forgotten there. Extending the wrapper mechanism is a nice proposal, I am open to this. @sertel : Do you want to switch parentheses and/or notations just for quickly looking at one goal or do you want to switch it for a few proof commands?

[hendriktews]

For extending the wrapper, I have the following remarks.

1. It does not work with C-c C-p to show the current goal.
2. There are many flags and users may sometimes want to switch a set of them, e.g., switching Implicit and Notations. This makes the user interface design challenging. (Magit uses the transient library to orchestrate all the git switches, but I find the interface cumbersome and I don't think we want to build on transient for the Coq flags.)
3. The wrapping does not (yet) work on the run-silent PR #762

[Matafou]

For extending the wrapper, I have the following remarks.

1. It does not work with C-c C-p to show the current goal.

Indeed. this should be easy to fix.

2. There are many flags and users may sometimes want to switch a set of them, e.g., switching Implicit _and_ Notations. This makes the user interface design challenging. (Magit uses the transient library to orchestrate all the git switches, but I find the interface cumbersome and I don't think we want to build on transient for the Coq flags.)

A solution would be that C-u should trigger a completion (+history) for a comma separated list of flags, defaulting to the last chosen one? My experience is that users tend to use the one or two same combinations all the time.

3. The wrapping does not (yet) work on the run-silent PR [Coq: run silently and explicitly Show when necessary - second attempt #762](https://github.com/ProofGeneral/PG/pull/762)

Indeed this needs some work to be compatible with this PR.

[sertel]

Most of the time I want to investigate the current goal including the context with notations turned off.

I'm not sure how relevant the key binding would be for because I'm using Spacemacs and hence would specifying something like SPC m c n or such.

[Matafou]

I never used spacemacs but it seems to also accept prefix args: type SPC u before typing the usual shortcut.

[Matafou]

Merging this in a few hours if noone objects. The question of keybindings remains. And also the global dealing with those options. Maybe we should have two menus: one for the coq session itself, and one for the queries specifically. I think vscoq has something like that: the "query" panel allows for flag switching that don't interfer with the session itself. But these questions should be answered elsewhere so let us merge this.

[hendriktews]

I like the idea to extend the wrapping mechanism, if a suitable completion works. I briefly looked into completion and only found completion commands that support to select one item out of a set or list. However, what we need here is completion to select a subset from a set (or a sublist from a list). This sounds like a nice Emacs hacking challenge, but it will take a while... Given this, I'll merge now. We can discuss again, when we have a solution for subset completion.

[Matafou]

On the wrapper: The idea is that the set of flags for queries is independent of the set of flags of the "session" (usual printing of goals and error messages). Using prefix arg says: use the special "query flags" instead of the "session flags". We can have a command to modify the set of query flags. This is more or less what is done in coqide and vscoq in the "query panel" (the set of checked boxes is transient). More generally we could even have several (numbered) sets of query flags and use the numerical prefix arg to trigger them.