[Agda] agda-mode input method

Frederik Hanghøj Iversen fhi.1990 at gmail.com
Thu Apr 26 15:31:17 CEST 2018


On Thu, Apr 26, 2018 at 3:02 PM, Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 2018-04-26 10:39, Frederik Hanghøj Iversen wrote:
>
>> Is there a way to make agda-input available without loading the Agda
>> itself.
>>
>
> The Agda input method is in a separate file, agda-input.el, which can be
> loaded independently. For instance, if you want to use the Agda input
> method in text mode, then you can include the following commands in your
> .emacs:
>
>   ;; Puts the directory with the Agda input method on the load path,
>   ;; among other things.
>   (load-file (let ((coding-system-for-read 'utf-8))
>                   (shell-command-to-string "agda-mode locate")))
>
>   ;; Loads the Agda input method.
>   (require 'agda-input)
>
>   ;; Enables the Agda input method when text mode is activated.
>   (add-hook 'text-mode-hook
>             (lambda nil (set-input-method "Agda")))
>
> --
> /NAD
>

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.

-- 
Regards
*Frederik Hanghøj Iversen*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180426/2b1f286f/attachment.html>


More information about the Agda mailing list