feat(emacs): literate agda org-mode support

This commit is contained in:
2025-12-05 12:57:12 -07:00
parent fb081d9d8e
commit d04348d9f2

View File

@@ -52,6 +52,10 @@
"K" #'agda2-goal-and-context)
(setq agda2-fontset-name "JuliaMono")
(add-to-list
'auto-mode-alist
'("\\.lagda\\.org\\'" . agda2-mode))
(with-eval-after-load 'smartparens
(sp-local-pair '(agda2-mode) "{!" "!}"))
(with-eval-after-load 'evil-surround
@@ -60,12 +64,23 @@
(setq-local evil-surround-pairs-alist
(append '((?h . ("{!" . "!}")))
evil-surround-pairs-alist)))))
;; HACK: avoid org-mode bullshit occuring in literate agda projects
;; within my roam dir.
(defun syd-agda--remove-org-roam-hooks-h ()
(when (and (featurep 'org-roam)
(string-match-p (rx ".lagda.org" eol)
(buffer-file-name)))
(remove-hook 'after-save-hook
#'org-roam-db-autosync--try-update-on-save-h t)))
(add-hook 'agda2-mode-hook #'syd-agda--remove-org-roam-hooks-h
-10)
(defun syd-agda-lookup-documentation ()
(interactive "P")
(call-interactively #'agda2-goal-and-context)
agda2-info-buffer)
(syd-handle 'agda2-mode
:docs #'syd-agda-lookup-documentation))
:docs #'syd-agda-lookup-documentation))
(provide 'syd/agda)