Skip to content

fix(agda): preserve input method in evil normal mode#8670

Open
kovan wants to merge 1 commit into
doomemacs:masterfrom
kovan:fix/agda-evil-input-method
Open

fix(agda): preserve input method in evil normal mode#8670
kovan wants to merge 1 commit into
doomemacs:masterfrom
kovan:fix/agda-evil-input-method

Conversation

@kovan

@kovan kovan commented Feb 13, 2026

Copy link
Copy Markdown
Contributor

Summary

  • Advise read-from-minibuffer and read-string to restore the input method from evil-input-method when in evil normal state
  • No-op when no input method is configured (checks evil-input-method first)
  • Guarded by (modulep! :editor evil)

Context

Fixes #5711. Evil clears current-input-method in normal state by design, storing the real method in evil-input-method. When agda2-mode calls read-string with INHERIT-INPUT-METHOD=t (e.g. for typecheck prompts), it inherits nil instead of the agda input method. Users must switch to insert mode first as a workaround.

Based on the workaround posted by @fdeitylink in the issue thread.

Test plan

  • Enable agda module with evil mode
  • Open an agda file, load it with agda2-load
  • In normal mode, invoke a command that opens a minibuffer prompt (e.g. refine, give)
  • Verify agda's quail input method translations work in the prompt
  • Verify normal buffers without input methods are unaffected

  • I searched the issue tracker and this hasn't been PRed before.
  • My changes are not on the do-not-PR list for this project.
  • My commits conform to Doom's git conventions.
  • I am blindly checking these off.
  • This PR contains AI-generated work.
  • Any relevant issues or PRs have been linked to.
  • This a draft PR; I need more time to finish it.

🤖 Generated with Claude Code

Evil clears `current-input-method' in normal state, storing the real
method in `evil-input-method'. This breaks agda's minibuffer prompts
that use `read-string' with INHERIT-INPUT-METHOD, as they inherit nil.
Advise `read-from-minibuffer' and `read-string' to restore the input
method from `evil-input-method' when in normal state.

Fix: doomemacs#5711

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

The typecheck prompt in agda2-mode does not recognize agda2-mode's quail translations

1 participant