[Agda] Certain Emacs commands not working; being reported as "undefined"

[Andrea Vezzosi]

Of course you can also call the commands by name, like

"M-x agda2-goal-and-context"

which is made much shorter by auto-completion

"M-x a-g-c"

Not sure If I advocate that, but it's good in a pinch and what I got used to.

Cheers,
Andrea


On Tue, Oct 16, 2018 at 7:09 PM Jason -Zhong Sheng- Hu
<fdhzs2010 at hotmail.com> wrote:
>
> I want to add a few more comments.
>
> Benjamin is correct. It's not a problem particular to whatever terminal emulator you use, but rather a fairly common problem with how terminals transmit key presses via a channel. This question, for example, has a good explanation of why some people use the term "terminal hell":
>
> https://superuser.com/questions/83166/using-c-m-to-do-a-query-replace-regexp-in-emacs-running-in-mac-terminal
>
> VT-100, for example, does not encode C-= at all: https://vt100.net/docs/vt100-ug/table3-5.html
>
> My personal experience, is emacs is impossible to work with via terminal without heavily remapping the key bindings. Normally emacs gestures rely on combinations of control key and meta key, and limited terminal encoding is just not pleasant to work with. I used to work with Vim, which is exceptionally nice to use in a terminal, but I find emacs isn't really friendly enough from that perspective.
>
> My suggestion is, emacs + terminal = unnecessary combat with limitations from old technologies. If you have a choice, it's better to work with GUI which has entire freedom of key strokes.
>
> Sincerely Yours,
>
> Jason Hu
> ________________________________
> From: Agda <agda-bounces at lists.chalmers.se> on behalf of Benjamin Price <benjamin.price at strath.ac.uk>
> Sent: October 16, 2018 12:43 PM
> To: agda at lists.chalmers.se
> Subject: Re: [Agda] Certain Emacs commands not working; being reported as "undefined"
>
> I'm guessing you are running Emacs in a terminal, rather than graphically?
>
> The problem is that when you press the `Ctrl` and `,` keys, the terminal treats it the same as if you only pressed `,` (and similarly for the other keys you listed).
> I.e. the keys Emacs receives are not the ones you thought you pressed.
>
> The easy fix is to map C-c = to the same function as C-c C-= (etc), so something like the following in your .emacs:
>
> (add-hook 'agda2-mode-hook
>           (lambda ()
>             (define-key agda2-mode-map (kbd "C-c ,") 'agda2-goal-and-context)
>             (define-key agda2-mode-map (kbd "C-c .") 'agda2-goal-and-context-and-inferred)
>             (define-key agda2-mode-map (kbd "C-c =") 'agda2-show-constraints)
>             (define-key agda2-mode-map (kbd "C-c ?") 'agda2-show-goals))
>
> ________________________________________
> From: Agda [agda-bounces at lists.chalmers.se] on behalf of Dave Martin [dave.martin at mail.com]
> Sent: 16 October 2018 17:10
> To: agda at lists.chalmers.se
> Subject: [Agda] Certain Emacs commands not working; being reported as "undefined"
>
> I have Agda 2.5.3 and Emacs 25.2.2. (I use the text version.)
>
> The following commands, and they alone as far as I know, do not work and are reported by Emacs as "C-c = is undefined" and so forth:
>
> C-c =
> C-c ?
> C-c ,
> C-c .
> C-c ;
>
> These are not typos; this--without the second cee-minus--is how the error messages appear for some reason. Meanwhile, most (often related) commands I have tried seem to work perfectly:
>
> C-c C-l
> C-x C-c
> C-c C-x C-d
> C-c C-f
> C-c C-b
> C-c C-d
> C-c C-n
>
> C-c C-SPC
> C-c C-r
> C-c C-a
> C-c C-c
> C-c C-t
> C-c C-e
>
> What might be the problem here?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda