[Agda] agda-mode input method

[John Leo]

Here's some code I got from Jennifer Paykin at UPenn to use Agda mode
standalone (via control-\) which is similar:

(condition-case nil
    (progn
      (load-file
       (let ((coding-system-for-read 'utf-8))
         (expand-file-name "agda-input.el"
                           (file-name-directory
                            (shell-command-to-string "agda-mode locate")))))

      (setq agda-input-user-translations '(("N" . ("ℕ"))))

      (agda-input-setup)
      (set-input-method "Agda"))

  (error
   (message "Could not load the Agda input method.")))


On Thu, Apr 26, 2018 at 2:43 AM, Sandro Stucki <sandro.stucki at gmail.com>
wrote:

> > 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
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180426/dadb4ad8/attachment.html>