doomemacs/modules/lang/agda/config.el

;;; lang/agda/config.el -*- lexical-binding: t; -*-

(when (and (modulep! +local)
           (executable-find "agda-mode"))
  (add-load-path!
   (file-name-directory (shell-command-to-string "agda-mode locate")))
  (unless (require 'agda2 nil t)
    (message "Failed to find the `agda2' package")))

(after! agda2-mode
  (set-lookup-handlers! 'agda2-mode
    :definition #'agda2-goto-definition-keyboard)

  (when (modulep! +tree-sitter)
    (set-tree-sitter-lang! 'agda2-mode 'agda)
    (add-hook! '(agda-mode-local-vars-hook
                 agda2-mode-local-vars-hook)
               :append #'tree-sitter!))

  (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)))
Added basic agda support. 2018-08-21 12:46:29 +02:00			`;;; lang/agda/config.el -- lexical-binding: t; --`

refactor: deprecate featurep! for modulep! featurep! will be renamed modulep! in the future, so it's been deprecated. They have identical interfaces, and can be replaced without issue. featurep! was never quite the right name for this macro. It implied that it had some connection to featurep, which it doesn't (only that it was similar in purpose; still, Doom modules are not features). To undo such implications and be consistent with its namespace (and since we're heading into a storm of breaking changes with the v3 release anyway), now was the best opportunity to begin the transition. 2022-08-12 20:29:19 +02:00			`(when (and (modulep! +local)`
lang/agda: add +local flag & :nonrecursive to recipes Relevant to #2203 2019-12-17 14:25:05 -05:00			`(executable-find "agda-mode"))`
			`(add-load-path!`
lang/agda: load agda2 if +local #2203 2019-12-18 10:12:41 -05:00			`(file-name-directory (shell-command-to-string "agda-mode locate")))`
			`(unless (require 'agda2 nil t)`
			(message "Failed to find the `agda2' package")))
lang/agda: add +local flag & :nonrecursive to recipes Relevant to #2203 2019-12-17 14:25:05 -05:00
add definition lookup handler to agda module 2020-09-28 02:10:29 +02:00			`(after! agda2-mode`
			`(set-lookup-handlers! 'agda2-mode`
			`:definition #'agda2-goto-definition-keyboard)`
refactor(:lang): move tree-sitter init Moved add-hook calls (for tree-sitter initialization) into their respective modes' config blocks, or nearby, to be consistent with how other, similar tools (like lsp!) are initialized, and does so at runtime, rather than at expansion/compile time, which eval-when! caused. 2022-07-25 17:34:44 +02:00
refactor: deprecate featurep! for modulep! featurep! will be renamed modulep! in the future, so it's been deprecated. They have identical interfaces, and can be replaced without issue. featurep! was never quite the right name for this macro. It implied that it had some connection to featurep, which it doesn't (only that it was similar in purpose; still, Doom modules are not features). To undo such implications and be consistent with its namespace (and since we're heading into a storm of breaking changes with the v3 release anyway), now was the best opportunity to begin the transition. 2022-08-12 20:29:19 +02:00			`(when (modulep! +tree-sitter)`
fix(agda): tree-sitter compatibility with agda2-mode Tree-sitter-lang recognized agda-mode, but not agda2-mode. 2022-09-10 15:01:11 +02:00			`(set-tree-sitter-lang! 'agda2-mode 'agda)`
refactor(:lang): move tree-sitter init Moved add-hook calls (for tree-sitter initialization) into their respective modes' config blocks, or nearby, to be consistent with how other, similar tools (like lsp!) are initialized, and does so at runtime, rather than at expansion/compile time, which eval-when! caused. 2022-07-25 17:34:44 +02:00			`(add-hook! '(agda-mode-local-vars-hook`
			`agda2-mode-local-vars-hook)`
			`:append #'tree-sitter!))`

add definition lookup handler to agda module 2020-09-28 02:10:29 +02:00			`(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)))`