Conveniently tweaking input method

Stream: Emacs

[Jason Reed]

Because of the discussion in #lean4 > Changing the abbreviation for `\n` I spent five minutes looking up how to make , the leading character for unicode entry in lean mode, so I thought I'd share what I found here: I added

(defun lean4-input-add-translations (trans)
  "Add the given translations TRANS to the Lean input method.
TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION).  The
translations are appended to the current translations."
  (with-temp-buffer
    (map-do (lambda (key tr)
              (when key
                (quail-defrule (concat "," key)
                               tr
                               "Lean" t)))
            trans)))

to my .emacs, after (require 'lean4-mode), and then putting (lean4-input-setup) in my lean4 mode hook. There might be a cleaner way of achieving this, but this works.

Relatedly, one could keep \ as the leading character and remove \n from the quail translations (more or less causing the same effect as the PR mentioned in the above thread) by doing

(defun lean4-input-add-translations (trans)
  "Add the given translations TRANS to the Lean input method.
TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION).  The
translations are appended to the current translations."
  (with-temp-buffer
    (map-do (lambda (key tr)
              (when (and key (not (equal key "n")))
                (quail-defrule (concat "\\" key)
                               tr
                               "Lean" t)))
            trans)))