[Agda] agda-mode input method

Frederik Hanghøj Iversen fhi.1990 at gmail.com
Thu Apr 26 10:39:38 CEST 2018


Is there a way to make agda-input available without loading the Agda itself.

I feel that the input mode is so generally useful that it ought to be
stand-alone.

On Thu, Apr 26, 2018 at 10:32 AM, Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 2018-04-26 10:28, Frederik Hanghøj Iversen wrote:
>
>> I'd like to use the input method that agda-mode ships with in other
>> major-modes. If I do `M-x set-input-method` Agda does not appear
>> anywhere on the list. Only after I engage `M-x agda2-mode` (and then
>> change back again) does it appear on the list.
>>
>> Can anyone more emacs-savvy than me explain why this is the case?
>>
>
> The Agda mode is typically not loaded when Emacs is started, but when an
> Agda file is opened, see agda2.el for implementation details.
>
> --
> /NAD
>



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


More information about the Agda mailing list