;;; syd-lang-idris2.el -*- lexical-binding: t; -*-

(require 'syd-handle-repl)
(require 'syd-handle-lookup)

(defun syd-idris2-open-repl ()
  (interactive)
  (idris2-repl-buffer))

(use-package idris2-mode
  :mode "\\.idr\\'"
  :straight (:type git
                   :host github
                   :repo "idris-community/idris2-mode")
  :config
  ;; Fixes lag when editing idris code with Evil.  See
  ;; https://github.com/idris-community/idris2-mode?tab=readme-ov-file#doom-emacs
  (syd-defadvice syd-idris2--fix-evil-motion-range (fn &rest args)
    "Like `evil-motion-range', but override field-beginning for performance.
See `https://github.com/ProofGeneral/PG/issues/427'."
    :around #'evil-motion-range
    (cl-letf (((symbol-function 'field-beginning)
               (lambda (&rest args) 1)))
      (apply fn args)))

  (add-hook 'idris2-mode-hook #'lsp)

  (general-define-key
   :keymaps 'idris2-mode-map
   :states '(normal visual motion emacs insert)
   :major-modes t
   :prefix syd-localleader-key
   :non-normal-prefix syd-alt-localleader-key
   "l" #'idris2-load-file)

  (set-repl-handler! 'idris2-mode
    #'syd-idris2-open-repl)

  (set-popup-rules!
    `((,(rx bol "*idris2-notes*" eol)
       :ttl nil)
      (,(rx bol "*idris2-holes*" eol)
       :ttl nil :quit t :vslot -5 :height 7)))
  (dolist (c '(?_ ??))
    (modify-syntax-entry c "w" idris2-syntax-table)))

(provide 'syd-lang-idris2)