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

(with-eval-after-load 'agda2
  (general-define-key
   :keymaps 'agda2-mode-map
   :states '(normal visual motion emacs insert)
   :major-modes t
   :prefix syd-localleader-key
   :non-normal-prefix syd-alt-localleader-key
   "?" #'agda2-show-goals
   "." #'agda2-goal-and-context-and-inferred
   "," #'agda2-goal-and-context
   "=" #'agda2-show-constraints
   "g" #'agda2-give
   "a" #'agda2-mimer-maybe-all
   "[" #'agda2-previous-goal
   "c" #'agda2-make-case
   "d" #'agda2-infer-type-maybe-toplevel
   "e" #'agda2-show-context
   "]" #'agda2-next-goal
   "h" #'agda2-helper-function-type
   "l" #'agda2-load
   "n" #'agda2-compute-normalised-maybe-toplevel
   "p" #'agda2-module-contents-maybe-toplevel
   "r" #'agda2-refine
   "s" #'agda2-solveAll
   "t" #'agda2-goal-type
   "w" #'agda2-why-in-scope-maybe-toplevel
   "x c" #'agda2-compile
   "x d" #'agda2-remove-annotations
   "x h" #'agda2-display-implicit-arguments
   "x q" #'agda2-quit
   "x r" #'agda2-restart)
  (general-def
    :keymaps 'agda2-mode-map
    :states '(motion normal)
    "[ n" #'agda2-previous-goal
    "] n" #'agda2-next-goal)
  (setq agda2-fontset-name "JuliaMono")

  ;; Inform Smartparens and Evil-surround of some extra brackets.
  (with-eval-after-load 'smartparens
    (sp-local-pair 'agda2-mode "⟨" "⟩"))
  (syd-add-hook 'agda2-mode-hook
    (defun syd-agda--configure-evil-surround-h ()
      (with-eval-after-load 'evil-surround
        (push '(?z . ("⟨" . "⟩"))
              evil-surround-pairs-alist))))

  (defun syd-agda-lookup-documentation ()
    (interactive)
    (call-interactively #'agda2-goal-and-context)
    agda2-info-buffer)

  ;; DEPRECATED: Remove once syd-strategies is working.
  (syd-add-hook 'agda2-mode-hook
    (defun syd-agda-set-handlers-h ()
      (setq-local syd-lookup-documentation-handlers
                  (list #'syd-agda-lookup-documentation)))))

(provide 'syd-lang-agda)