From 88fc0549193de923a73d75a10ab055e22fb34f2b Mon Sep 17 00:00:00 2001
From: Rudi Grinberg <rudi.grinberg@gmail.com>
Date: Thu, 29 Aug 2019 20:07:41 +0700
Subject: [PATCH] Use straight for agda

We can fetch the mode directly from straight. There's no need to rely on
having this .el file installed for us. Now agda's el files can be edited
directly like all other emacs packages.

Signed-off-by: Rudi Grinberg <rudi.grinberg@gmail.com>
---
 modules/lang/agda/config.el   | 69 +++++++++++++++--------------------
 modules/lang/agda/doctor.el   |  5 ---
 modules/lang/agda/packages.el | 15 ++++++++
 3 files changed, 45 insertions(+), 44 deletions(-)
 delete mode 100644 modules/lang/agda/doctor.el
 create mode 100644 modules/lang/agda/packages.el

diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el
index 715e33658..e2cb6ad4a 100644
--- a/modules/lang/agda/config.el
+++ b/modules/lang/agda/config.el
@@ -1,41 +1,32 @@
 ;;; lang/agda/config.el -*- lexical-binding: t; -*-
 
-(defvar +agda-dir
-  (when (executable-find "agda-mode")
-    (file-name-directory (shell-command-to-string "agda-mode locate"))))
-
-(use-package! agda2
-  :when +agda-dir
-  :load-path +agda-dir)
-
-(use-package! agda2-mode
-  :defer t
-  :config
-  (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)))
+(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))
diff --git a/modules/lang/agda/doctor.el b/modules/lang/agda/doctor.el
deleted file mode 100644
index e38ccbc03..000000000
--- a/modules/lang/agda/doctor.el
+++ /dev/null
@@ -1,5 +0,0 @@
-;; -*- lexical-binding: t; no-byte-compile: t; -*-
-;;; lang/agda/doctor.el
-
-(unless (executable-find "agda-mode")
-  (warn! "Couldn't find agda-mode. Agda support won't work"))
diff --git a/modules/lang/agda/packages.el b/modules/lang/agda/packages.el
new file mode 100644
index 000000000..35bead2a1
--- /dev/null
+++ b/modules/lang/agda/packages.el
@@ -0,0 +1,15 @@
+;; -*- no-byte-compile: t; -*-
+;;; lang/agda/packages.el
+
+
+(package! agda-input
+  :recipe
+  (:host github :repo "agda/agda"
+         :files ("src/data/emacs-mode/agda-input.el")))
+
+(package! agda2-mode
+  :recipe
+  (:host github :repo "agda/agda"
+         :files
+         ("src/data/emacs-mode/*.el"
+          (:exclude "agda-input.el"))))