<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Thu, Apr 26, 2018 at 3:02 PM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 2018-04-26 10:39, Frederik Hanghøj Iversen wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Is there a way to make agda-input available without loading the Agda<br>
itself.<br>
</blockquote>
<br></span>
The Agda input method is in a separate file, agda-input.el, which can be<br>
loaded independently. For instance, if you want to use the Agda input<br>
method in text mode, then you can include the following commands in your<br>
.emacs:<br>
<br>
  ;; Puts the directory with the Agda input method on the load path,<br>
  ;; among other things.<span class=""><br>
  (load-file (let ((coding-system-for-read 'utf-8))<br>
                  (shell-command-to-string "agda-mode locate")))<br>
<br></span>
  ;; Loads the Agda input method.<br>
  (require 'agda-input)<br>
<br>
  ;; Enables the Agda input method when text mode is activated.<br>
  (add-hook 'text-mode-hook<br>
            (lambda nil (set-input-method "Agda")))<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br>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.<br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div>Regards</div><div><i>Frederik Hanghøj Iversen</i></div></div>
</div></div>