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

[Dave Martin]

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?

[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-***@lists.chalmers.se] on behalf of Dave Martin [***@mail.com]
Sent: 16 October 2018 17:10
To: ***@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?

[Jason -Zhong Sheng- Hu]

This post might be inappropriate. Click to display it.

[Andrea Vezzosi]

This post might be inappropriate. Click to display it.