[Agda] agda-mode input method

[Sandro Stucki]

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

The input method is in a separate file "agda-input", so I guess it can
be used standalone in principle. Of course, you still need to tell
emacs how to find the file. So you could include something like this
in your .emacs file:

  (add-to-list 'load-path "<path-to-Agda-installation>/emacs-mode/")
  (require 'agda-input nil t)

But that's a bit brittle, so it's probably better to just load
agda-mode the usual way:

  (load-file (let ((coding-system-for-read 'utf-8))
               (shell-command-to-string "agda-mode locate")))
  (require 'agda-input nil t)

If you just want unicode support you could also use the "TeX" input
method (though personally, I prefer the Agda input method).

Cheers
/Sandro


On Thu, Apr 26, 2018 at 10:39 AM, Frederik Hanghøj Iversen
<fhi.1990 at gmail.com> wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>