Missing top command `CornelisShowConstraints` (Emacs `C-c C-=`)

[andreasabel]

Feature request: add CornelisShowConstraints, equivalent of Emacs C-c C-=.
This displays the solution for the interaction metas that have been found by unification (if any).
It is the command Cmd_constraints of the Agda interaction server.
https://github.com/agda/agda/blob/822e0aee235ba787b7ac50cc7ab19fca20be5924/src/full/Agda/Interaction/InteractionTop.hs#L505-L506

[4e554c4c]

Agree, this would be a nice feature.

[4e554c4c]

I've started work on this since I was working in a file with some constraints.

It's actually a huge pain since Cornelis is essentially the only client that communicates with Agda over json. Agda formats constraints on the Emacs interaction channel, but not on the json channel. So we essentially need to rebuild the formatting for every constraint from scratch (and copy a lot of code from Agda).

I'll try to post a WIP soon.

[andreasabel]

Cornelis is essentially the only client that communicates with Agda over json.

Ah, good to know, I thought --interaction-json didn't have any users anymore.

Agda formats constraints on the Emacs interaction channel, but not on the json channel.

Maybe this should be fixed upstream (in Agda) instead?

[4e554c4c]

I considered that, but in that case other commands (like show goals) should also be formatted on the agda side

and that would break the protocol just like the v2.7.0->v2.8.0 version did... which was a lot of pain (see #169)

it might be easier for us to switch to the elisp backend, just like the vscode plugin does.