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

[Jason -Zhong Sheng- Hu]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181016/85c4a9ef/attachment.html>