From d04348d9f2edb270d34dafef1f8873f12339fad3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Madeleine=20Sydney=20=C5=9Alaga?= Date: Fri, 5 Dec 2025 12:57:12 -0700 Subject: [PATCH] feat(emacs): literate agda org-mode support --- modules/home/users/msyds/emacs/lisp/syd/agda.el | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/modules/home/users/msyds/emacs/lisp/syd/agda.el b/modules/home/users/msyds/emacs/lisp/syd/agda.el index b753d12..21ba724 100755 --- a/modules/home/users/msyds/emacs/lisp/syd/agda.el +++ b/modules/home/users/msyds/emacs/lisp/syd/agda.el @@ -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)