emenel/doomemacs
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Merge pull request #1731 from rgrinberg/agda-straight

Browse source 
lang/agda: install agda2-mode via straight
This commit is contained in:
Henrik Lissner 2019-09-02 00:45:56 -04:00 • committed by GitHub
commit 6254829d46
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 45 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

69
modules/lang/agda/config.el
View file

@ -1,41 +1,32 @@
;;; lang/agda/config.el -*- lexical-binding: t; -*- ;;; lang/agda/config.el -*- lexical-binding: t; -*-
(defvar +agda-dir (map!
(when (executable-find "agda-mode") :after agda2-mode
(file-name-directory (shell-command-to-string "agda-mode locate")))) :map agda2-mode-map
:localleader
(use-package! agda2 "?" #'agda2-show-goals
:when +agda-dir "." #'agda2-goal-and-context-and-inferred
:load-path +agda-dir) "," #'agda2-goal-and-context
"=" #'agda2-show-constraints
(use-package! agda2-mode "SPC" #'agda2-give
:defer t "a" #'agda2-auto-maybe-all
:config "b" #'agda2-previous-goal
(map! :map agda2-mode-map "c" #'agda2-make-case
:localleader "d" #'agda2-infer-type-maybe-toplevel
"?" #'agda2-show-goals "e" #'agda2-show-context
"." #'agda2-goal-and-context-and-inferred "f" #'agda2-next-goal
"," #'agda2-goal-and-context "gG" #'agda2-go-back
"=" #'agda2-show-constraints "h" #'agda2-helper-function-type
"SPC" #'agda2-give "l" #'agda2-load
"a" #'agda2-auto-maybe-all "n" #'agda2-compute-normalised-maybe-toplevel
"b" #'agda2-previous-goal "p" #'agda2-module-contents-maybe-toplevel
"c" #'agda2-make-case "r" #'agda2-refine
"d" #'agda2-infer-type-maybe-toplevel "s" #'agda2-solveAll
"e" #'agda2-show-context "t" #'agda2-goal-type
"f" #'agda2-next-goal "w" #'agda2-why-in-scope-maybe-toplevel
"gG" #'agda2-go-back (:prefix "x"
"h" #'agda2-helper-function-type "c" #'agda2-compile
"l" #'agda2-load "d" #'agda2-remove-annotations
"n" #'agda2-compute-normalised-maybe-toplevel "h" #'agda2-display-implicit-arguments
"p" #'agda2-module-contents-maybe-toplevel "q" #'agda2-quit
"r" #'agda2-refine "r" #'agda2-restart))
"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)))

5
modules/lang/agda/doctor.el
View file

@ -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"))

15
modules/lang/agda/packages.el Normal file
View file

@ -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"))))