[Agda] agda-mode input method

[Frederik Hanghøj Iversen]

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?

I can think of at least two useful places to have agda's input method:
Haskell with UnicodeSyntax and latex with \usepackage{unicode-math}.

[Nils Anders Danielsson]

Post by Frederik Hanghøj Iversen
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.

[Frederik Hanghøj Iversen]

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.

Post by Nils Anders Danielsson

Post by Frederik Hanghøj Iversen
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

[Sandro Stucki]

Post by Frederik Hanghøj Iversen
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

Post by Frederik Hanghøj Iversen
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.

Post by Nils Anders Danielsson

Post by Frederik Hanghøj Iversen
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
https://lists.chalmers.se/mailman/listinfo/agda

[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.")))

Post by Frederik Hanghøj Iversen

Post by Frederik Hanghøj Iversen
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
(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
(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

Post by Frederik Hanghøj Iversen
Is there a way to make agda-input available without loading the Agda

itself.

Post by Frederik Hanghøj Iversen
I feel that the input mode is so generally useful that it ought to be
stand-alone.

Post by Nils Anders Danielsson

Post by Frederik Hanghøj Iversen
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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Nils Anders Danielsson]

Post by Frederik Hanghøj Iversen
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")))

[Frederik Hanghøj Iversen]

Post by Nils Anders Danielsson

Post by Frederik Hanghøj Iversen
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
;; 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.

[Nils Anders Danielsson]

Post by Frederik Hanghøj Iversen
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.

I based the Agda input method on the TeX input method. The following
(customisable) part of the code specifies exactly how:

(defcustom agda-input-inherit
`(("TeX" . (agda-input-compose
(agda-input-drop '("geq" "leq" "bullet" "qed" "par"))
(agda-input-or
(agda-input-drop-prefix "\\")
(agda-input-or
(agda-input-compose
(agda-input-drop '("^l" "^o" "^r" "^v"))
(agda-input-prefix "^"))
(agda-input-prefix "_")))))
)
[...])

In words:

* Keep bindings that start with _.
* Keep bindings that start with ^, except for ^l, ^o, ^r and ^v.
* Keep bindings that start with \, and drop this prefix.
* Remove geq, leq, bullet, qed and par from the bindings above.

These bindings are combined with bindings specific to the Agda input
method (these are customisable). Finally another part of the code (also
customisable) removes empty bindings and prepends \ to all bindings.