From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: Amin Bandali Newsgroups: gmane.emacs.help Subject: Re: [OFFTOPIC] Re: Invoking a function from a list of functions Date: Tue, 20 Nov 2018 01:15:31 -0500 Message-ID: <87sgzwl1fg.fsf@aminb.org> References: <67c4a534-d41c-4736-8839-c2dbbdf7f9c2@googlegroups.com> <2da7504a-8bbf-41b9-993e-a7bacd6c97b2@googlegroups.com> <20181116114002.3ba6bcc8dc1e699ba58e08b8@speakeasy.net> <20181119172358.802ce30c54f2fd20f8c300c4@speakeasy.net> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Trace: blaine.gmane.org 1542694490 24563 195.159.176.226 (20 Nov 2018 06:14:50 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Tue, 20 Nov 2018 06:14:50 +0000 (UTC) User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.0.50 (gnu/linux) Cc: help-gnu-emacs@gnu.org To: Stefan Monnier Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Tue Nov 20 07:14:46 2018 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gOzJ7-0006Gt-2N for geh-help-gnu-emacs@m.gmane.org; Tue, 20 Nov 2018 07:14:45 +0100 Original-Received: from localhost ([::1]:60352 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gOzLD-0005GY-Kg for geh-help-gnu-emacs@m.gmane.org; Tue, 20 Nov 2018 01:16:55 -0500 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:38090) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gOzK0-0004wD-1K for help-gnu-emacs@gnu.org; Tue, 20 Nov 2018 01:15:41 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gOzJz-0001Es-5E for help-gnu-emacs@gnu.org; Tue, 20 Nov 2018 01:15:40 -0500 Original-Received: from fencepost.gnu.org ([2001:4830:134:3::e]:43505) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gOzJs-00017O-M0; Tue, 20 Nov 2018 01:15:32 -0500 Original-Received: from wn-res-nat-129-97-125-1.dynamic.uwaterloo.ca ([129.97.125.1]:13492 helo=localhost) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1gOzJs-0003a9-H6; Tue, 20 Nov 2018 01:15:32 -0500 In-Reply-To: (Stefan Monnier's message of "Mon, 19 Nov 2018 18:11:44 -0500") X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.21 Precedence: list List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Original-Sender: "help-gnu-emacs" Xref: news.gmane.org gmane.emacs.help:118720 Archived-At: Stefan Monnier writes: > FWIW, in the Agda language, it's very common to use non-ASCII characters > which are input (in agda-mode) via a variant of the TeX input method. > The reason this is tolerated is because those chars are already familiar > to most users because they're used on paper for the same purpose. Same with Lean: lean-mode comes with lean-input which is based on agda-input with minor changes, and it makes it /super/ convenient to insert commonly used unicode characters: \a for =CE=B1, \b for =CE=B2, a\1 for a=E2=82=81, \and for =E2=88=A7, \|- for =E2=8A=A2, and hundreds mor= e. I=E2=80=99ve actually come to like lean-input so much that I=E2=80=99ve set it as my default-input-method so I can toggle it with C-\ and easily type unicode symbols whenever and wherever I want. I=E2=80=99ve been experimenting with using lean-input along with the unicode-math package (for {Lua,Xe}TeX) and it has drastically improved my experience with writing and reading Org and TeX documents. It=E2=80=99s possible to change the input prefix from backslash to something else to avoid clashes when writing TeX=C2=B9. Footnotes: =C2=B9 https://git.sr.ht/~bandali/dotfiles/commit/e44b9b7eb100a3d5c1640b7d= f7d4c458f81998ab