agda-mode: Make unicode play well with evil-mode

[ghost]

Unicode input does not work in normalisation (via C-c C-n) or typechecking (C-c C-d) when using evil-mode.

To demonstrate this, install agda-mode and evil-mode, require evil-mode and load-file agda-mode, then open an Agda source file where you M-x evil-mode, and try to C-c C-n with e.g. '\bn'. Spoiler alert: you'll end up typing literally '\bn'.

[ghost]

Using unicode in the regular /-search would also be beneficial.

[andreasabel]

I do not know evil-mode, but the Agda input method can be toggled by C-\ (e.g. turned on for search after C-s).

[ghost]

I am able to reproduce this when evil-mode is disabled.

Furthermore, if I run with (require 'evil-mode), open an Agda program, and run (turn-on-evil-mode), it still works. It even works using evil-mode's /-search. It also works in the normaliser and in the typechecker.

But, if you have (evil-mode 1) in your configuration, which turns on evil-mode globally -- it doesn't work in search. I don't know why this is significant. It's all very confusing.

The good news is that your C-\ tips always works for the normaliser and in the typechecker, even with evil-mode, so that's a godsend. Now if only search would be a little bit more collaborative as well.

[andreasabel]

Shooting in the dark: could it be that if evil-mode is on globally, then the C-\ functionality is bound to something else globally, even in the search minibuffer?! [Not very consistent with the fact it works in Agda interaction though...]

Unfortunately, I am not good a emacs-lisp and I am not a vi user at all. Maybe @UlfNorell knows something, he is a vi user.

[ghost]

Interestingly C-h k C-\ says "C-\ runs the command toggle-input-method". I'm not an advanced emacs user yet, so I'm not sure how I can check what C-\ is bound to at the moment of attempting to search (either via / or via C-s). Amusingly, I found out that C-h d supports C-\ for some reason. It's all seemingly quite random to me as an inexperienced user.

[UlfNorell]

I'm a vi user, but not an emacs user (except for Agda coding) and no evil-mode experience.

[nad]

Let's try to figure out where the problem lies.

Load the following code (by placing the cursor right after the final closing parenthesis and typing M-x eval-last-sexp RET):

(defun quick-test (argument)
  "Prints ARGUMENT."
  (interactive "MWrite something: ")
  (message "%s" argument))

Now execute the code (using M-x quick-test RET) when evil-mode and the Agda input method are both active. Is the input method preserved? If not, then I don't think that the Agda mode is to blame.

[ghost]

I'm not sure what you mean by "preserved", but I can indeed activate it in this prompt.

[nad]

I interpret your response as saying that, despite the Agda input method being active just before you run quick-test, it is not initially active in the minibuffer. This suggests to me that evil-mode messes with the input method in some way.

[ibbem]

I've experienced the same issue. It's correct that evil is the problem in this case. I opened a pull request addressing this issue.

In the meantime, for everyone who is annoyed by this: Putting the following code snippet in your Emacs config solves this issue (eliminates the need for pressing C-\ on each new Agda buffer).

(defun set-agda-input-method ()
  (evil-without-input-method-hooks ;; Disable evil's hooks which reset current-input-method in favor of evil-input-method before the evil minor mode has been loaded.
    (set-input-method "Agda")))
(add-hook 'agda2-mode-hook 'set-agda-input-method)

[pmbittner]

This works for me! Thank you so much. 😃

GNU Emacs 28.1
Spacemacs v.0.999.0