From 1fa4516caddd2e04bb443b5e67df5ae898c75d2e Mon Sep 17 00:00:00 2001
From: bottomtype <falsityproven@gmail.com>
Date: Mon, 28 Sep 2020 02:10:29 +0200
Subject: [PATCH] add definition lookup handler to agda module

---
 modules/lang/agda/config.el | 61 +++++++++++++++++++------------------
 1 file changed, 31 insertions(+), 30 deletions(-)

diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el
index d54bddc3b..212a9b5e1 100644
--- a/modules/lang/agda/config.el
+++ b/modules/lang/agda/config.el
@@ -7,33 +7,34 @@
   (unless (require 'agda2 nil t)
     (message "Failed to find the `agda2' package")))
 
-
-(map! :after agda2-mode
-      :map agda2-mode-map
-      :localleader
-      "?"   #'agda2-show-goals
-      "."   #'agda2-goal-and-context-and-inferred
-      ","   #'agda2-goal-and-context
-      "="   #'agda2-show-constraints
-      "SPC" #'agda2-give
-      "a"   #'agda2-auto-maybe-all
-      "b"   #'agda2-previous-goal
-      "c"   #'agda2-make-case
-      "d"   #'agda2-infer-type-maybe-toplevel
-      "e"   #'agda2-show-context
-      "f"   #'agda2-next-goal
-      "gG"  #'agda2-go-back
-      "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
-      (:prefix "x"
-        "c"   #'agda2-compile
-        "d"   #'agda2-remove-annotations
-        "h"   #'agda2-display-implicit-arguments
-        "q"   #'agda2-quit
-        "r"   #'agda2-restart))
+(after! agda2-mode
+  (set-lookup-handlers! 'agda2-mode
+    :definition #'agda2-goto-definition-keyboard)
+  (map! :map agda2-mode-map
+        :localleader
+        "?"   #'agda2-show-goals
+        "."   #'agda2-goal-and-context-and-inferred
+        ","   #'agda2-goal-and-context
+        "="   #'agda2-show-constraints
+        "SPC" #'agda2-give
+        "a"   #'agda2-auto-maybe-all
+        "b"   #'agda2-previous-goal
+        "c"   #'agda2-make-case
+        "d"   #'agda2-infer-type-maybe-toplevel
+        "e"   #'agda2-show-context
+        "f"   #'agda2-next-goal
+        "gG"  #'agda2-go-back
+        "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
+        (:prefix "x"
+          "c"   #'agda2-compile
+          "d"   #'agda2-remove-annotations
+          "h"   #'agda2-display-implicit-arguments
+          "q"   #'agda2-quit
+          "r"   #'agda2-restart)))