[Agda] agda-mode input method

[Nils Anders Danielsson]

On 2018-04-26 15:31, Frederik Hanghøj Iversen wrote:
> This looks like the sort of thing I was going for. I'll give it a try.
> Thank you! I'll also give the TeX-input method a try.

I based the Agda input method on the TeX input method. The following
(customisable) part of the code specifies exactly how:

   (defcustom agda-input-inherit
     `(("TeX" . (agda-input-compose
                 (agda-input-drop '("geq" "leq" "bullet" "qed" "par"))
                 (agda-input-or
                  (agda-input-drop-prefix "\\")
                  (agda-input-or
                   (agda-input-compose
                    (agda-input-drop '("^l" "^o" "^r" "^v"))
                    (agda-input-prefix "^"))
                   (agda-input-prefix "_")))))
       )
     [...])

In words:

* Keep bindings that start with _.
* Keep bindings that start with ^, except for ^l, ^o, ^r and ^v.
* Keep bindings that start with \, and drop this prefix.
* Remove geq, leq, bullet, qed and par from the bindings above.

These bindings are combined with bindings specific to the Agda input
method (these are customisable). Finally another part of the code (also
customisable) removes empty bindings and prepends \ to all bindings.

-- 
/NAD