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

[Benjamin Price]

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