<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
I want to add a few more comments.</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
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":</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<a href="https://superuser.com/questions/83166/using-c-m-to-do-a-query-replace-regexp-in-emacs-running-in-mac-terminal" id="LPNoLP619564">https://superuser.com/questions/83166/using-c-m-to-do-a-query-replace-regexp-in-emacs-running-in-mac-terminal</a><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
VT-100, for example, does not encode C-= at all: <a href="https://vt100.net/docs/vt100-ug/table3-5.html" id="LPNoLP796632">
https://vt100.net/docs/vt100-ug/table3-5.html</a><br>
</div>
<br>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
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.</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
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.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="signature">
<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<div><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>
</b></span></span></font></div>
<font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>
Jason Hu<a target="_blank"></a></b></span></span></font> </div>
</div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Benjamin Price <benjamin.price@strath.ac.uk><br>
<b>Sent:</b> October 16, 2018 12:43 PM<br>
<b>To:</b> agda@lists.chalmers.se<br>
<b>Subject:</b> Re: [Agda] Certain Emacs commands not working; being reported as "undefined"</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">I'm guessing you are running Emacs in a terminal, rather than graphically?<br>
<br>
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).<br>
I.e. the keys Emacs receives are not the ones you thought you pressed.<br>
<br>
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:<br>
<br>
(add-hook 'agda2-mode-hook<br>
(lambda ()<br>
(define-key agda2-mode-map (kbd "C-c ,") 'agda2-goal-and-context)<br>
(define-key agda2-mode-map (kbd "C-c .") 'agda2-goal-and-context-and-inferred)<br>
(define-key agda2-mode-map (kbd "C-c =") 'agda2-show-constraints)<br>
(define-key agda2-mode-map (kbd "C-c ?") 'agda2-show-goals))<br>
<br>
________________________________________<br>
From: Agda [agda-bounces@lists.chalmers.se] on behalf of Dave Martin [dave.martin@mail.com]<br>
Sent: 16 October 2018 17:10<br>
To: agda@lists.chalmers.se<br>
Subject: [Agda] Certain Emacs commands not working; being reported as "undefined"<br>
<br>
I have Agda 2.5.3 and Emacs 25.2.2. (I use the text version.)<br>
<br>
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:<br>
<br>
C-c =<br>
C-c ?<br>
C-c ,<br>
C-c .<br>
C-c ;<br>
<br>
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:<br>
<br>
C-c C-l<br>
C-x C-c<br>
C-c C-x C-d<br>
C-c C-f<br>
C-c C-b<br>
C-c C-d<br>
C-c C-n<br>
<br>
C-c C-SPC<br>
C-c C-r<br>
C-c C-a<br>
C-c C-c<br>
C-c C-t<br>
C-c C-e<br>
<br>
What might be the problem here?<br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</span></font></div>
</body>
</html>