feat(emacs): Agda

modules/home/users/msyds/emacs/lisp/syd/agda.el

@@ -0,0 +1,61 @@
+;;; -*- lexical-binding: t -*-
+
+(require 'syd/base)
+(require 'syd/handle)
+
+(defun syd-agda-locate-and-load ()
+  (interactive)
+  (let ((agda-mode-path (executable-find "agda-mode")))
+    (load-file
+     (shell-command-to-string
+      (format "%s locate" agda-mode-path))))
+  (setq agda2-program-name (executable-find "agda")))
+
+(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")
+
+  (defun syd-agda-lookup-documentation ()
+    (interactive)
+    (call-interactively #'agda2-goal-and-context)
+    agda2-info-buffer)
+
+  ;; DEPRECATED: Remove once syd-strategies is working.
+  (syd-handle 'agda2-mode
+              :docs #'syd-agda-lookup-documentation))
+
+(provide 'syd/agda)

modules/home/users/msyds/emacs/lisp/syd/smartparens.el

@@ -51,6 +51,10 @@ It is only enabled it if `smartparens-global-mode' is on."
   ;; You're likely writing lisp in the minibuffer, therefore, disable these
   ;; quote pairs, which lisps doesn't use for strings:
   (sp-local-pair '(minibuffer-mode minibuffer-inactive-mode) "'" nil :actions nil)
-  (sp-local-pair '(minibuffer-mode minibuffer-inactive-mode) "`" nil :actions nil))
+  (sp-local-pair '(minibuffer-mode minibuffer-inactive-mode) "`" nil :actions nil)
+  (dolist (pair '(("⟨" "⟩")
+                  ("⟪" "⟫")
+                  ("⟅" "⟆")))
+    (sp-local-pair 'fundamental-mode (car pair) (cdr pair))))
 
 (provide 'syd/smartparens)