From b3a83daf5f6ad95841741d84cc33145a9d354d1e Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Tue, 21 Aug 2018 12:46:29 +0200 Subject: [PATCH 1/9] Added basic agda support. --- modules/lang/agda/README.org | 9 +++++++++ modules/lang/agda/config.el | 7 +++++++ modules/lang/agda/doctor.el | 5 +++++ 3 files changed, 21 insertions(+) create mode 100644 modules/lang/agda/README.org create mode 100644 modules/lang/agda/config.el create mode 100644 modules/lang/agda/doctor.el diff --git a/modules/lang/agda/README.org b/modules/lang/agda/README.org new file mode 100644 index 000000000..1812f748d --- /dev/null +++ b/modules/lang/agda/README.org @@ -0,0 +1,9 @@ +#+TITLE: :lang agda + +This module adds support for the [[http://wiki.portal.chalmers.se/agda/pmwiki.php][agda]] programming language. + +Emacs support is included in the agda release (you can find installation +instructions [[https://agda.readthedocs.io/en/latest/getting-started/installation.html][here]]). This module attempts to find the location of ~agda2.el~ via +the ~agda-mode locate~ command that comes with the agda release. Users can set +this manually by setting the ~+agda2-dir~ variable. + diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el new file mode 100644 index 000000000..a294c30f7 --- /dev/null +++ b/modules/lang/agda/config.el @@ -0,0 +1,7 @@ +;;; lang/agda/config.el -*- lexical-binding: t; -*- + +(defvar +agda-dir (string-remove-suffix "/agda2.el" (shell-command-to-string "agda-mode locate"))) + +(def-package! agda2 + :load-path +agda-dir) + diff --git a/modules/lang/agda/doctor.el b/modules/lang/agda/doctor.el new file mode 100644 index 000000000..e38ccbc03 --- /dev/null +++ b/modules/lang/agda/doctor.el @@ -0,0 +1,5 @@ +;; -*- 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")) From 06262fef1761d0f7018e5c2991853687b7f53be8 Mon Sep 17 00:00:00 2001 From: Henrik Lissner Date: Wed, 22 Aug 2018 03:52:53 +0200 Subject: [PATCH 2/9] Lazy-load agda2; more robust +agda-dir resolution --- modules/lang/agda/config.el | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el index a294c30f7..6166727b9 100644 --- a/modules/lang/agda/config.el +++ b/modules/lang/agda/config.el @@ -1,7 +1,11 @@ ;;; lang/agda/config.el -*- lexical-binding: t; -*- -(defvar +agda-dir (string-remove-suffix "/agda2.el" (shell-command-to-string "agda-mode locate"))) +(defvar +agda-dir + (when (executable-find "adga-mode") + (file-name-directory (shell-command-to-string "agda-mode locate"))) + "TODO") + (def-package! agda2 - :load-path +agda-dir) - + :load-path +agda-dir + :defer t) From f6dbc00bc4abb6790f6bfe31f254213c06c1dba8 Mon Sep 17 00:00:00 2001 From: Henrik Lissner Date: Wed, 22 Aug 2018 03:53:19 +0200 Subject: [PATCH 3/9] Fix agda-mode executable typo --- modules/lang/agda/config.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el index 6166727b9..cd355d43c 100644 --- a/modules/lang/agda/config.el +++ b/modules/lang/agda/config.el @@ -1,7 +1,7 @@ ;;; lang/agda/config.el -*- lexical-binding: t; -*- (defvar +agda-dir - (when (executable-find "adga-mode") + (when (executable-find "agda-mode") (file-name-directory (shell-command-to-string "agda-mode locate"))) "TODO") From f6d6096bf253290a03375053a74c306ca5a14728 Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Sat, 25 Aug 2018 17:27:42 +0200 Subject: [PATCH 4/9] load agda input method; bypass agda2; keybindings --- modules/lang/agda/config.el | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el index cd355d43c..cb1a92f2e 100644 --- a/modules/lang/agda/config.el +++ b/modules/lang/agda/config.el @@ -2,10 +2,18 @@ (defvar +agda-dir (when (executable-find "agda-mode") - (file-name-directory (shell-command-to-string "agda-mode locate"))) - "TODO") + (file-name-directory (shell-command-to-string "agda-mode locate")))) +(def-package! agda-input + :load-path +agda-dir) -(def-package! agda2 - :load-path +agda-dir - :defer t) +(def-package! agda2-mode + :mode "\\.agda\\'" + :after agda-input + :config + (map! :map agda2-mode-map + :localleader + :n "l" #'agda2-load + :n "d" #'agda2-infer-type-maybe-toplevel + :n "o" #'agda2-module-contents-maybe-toplevel + :n "n" #'agda2-compute-normalised-maybe-toplevel)) From 82651f247eaf57a550740792fcc2e02f4e3c443f Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Mon, 3 Sep 2018 13:54:49 +0200 Subject: [PATCH 5/9] Fix syntax highlighting --- modules/lang/agda/config.el | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el index cb1a92f2e..f44e235db 100644 --- a/modules/lang/agda/config.el +++ b/modules/lang/agda/config.el @@ -10,6 +10,21 @@ (def-package! agda2-mode :mode "\\.agda\\'" :after agda-input + :init + ;; fix syntax highlighting + ;; (taken from https://github.com/syl20bnr/spacemacs/blob/develop/layers/%2Blang/agda/packages.el) + (progn + (mapc + (lambda (x) (add-to-list 'face-remapping-alist x)) + '((agda2-highlight-datatype-face . font-lock-type-face) + (agda2-highlight-function-face . font-lock-type-face) + (agda2-highlight-inductive-constructor-face . font-lock-function-name-face) + (agda2-highlight-keyword-face . font-lock-keyword-face) + (agda2-highlight-module-face . font-lock-constant-face) + (agda2-highlight-number-face . nil) + (agda2-highlight-postulate-face . font-lock-type-face) + (agda2-highlight-primitive-type-face . font-lock-type-face) + (agda2-highlight-record-face . font-lock-type-face)))) :config (map! :map agda2-mode-map :localleader @@ -17,3 +32,4 @@ :n "d" #'agda2-infer-type-maybe-toplevel :n "o" #'agda2-module-contents-maybe-toplevel :n "n" #'agda2-compute-normalised-maybe-toplevel)) + ;; TODO finish keybindings From 17f0b4c50e67f006d7333d8aca0dc6759d5f5575 Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Mon, 3 Sep 2018 15:45:43 +0200 Subject: [PATCH 6/9] Update syntax highlighting --- modules/lang/agda/config.el | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el index f44e235db..ea753aec7 100644 --- a/modules/lang/agda/config.el +++ b/modules/lang/agda/config.el @@ -16,15 +16,23 @@ (progn (mapc (lambda (x) (add-to-list 'face-remapping-alist x)) - '((agda2-highlight-datatype-face . font-lock-type-face) - (agda2-highlight-function-face . font-lock-type-face) - (agda2-highlight-inductive-constructor-face . font-lock-function-name-face) - (agda2-highlight-keyword-face . font-lock-keyword-face) - (agda2-highlight-module-face . font-lock-constant-face) - (agda2-highlight-number-face . nil) - (agda2-highlight-postulate-face . font-lock-type-face) - (agda2-highlight-primitive-type-face . font-lock-type-face) - (agda2-highlight-record-face . font-lock-type-face)))) + '((agda2-highlight-keyword-face . font-lock-keyword-face) + (agda2-highlight-string-face . font-lock-string-face) + (agda2-highlight-number-face . font-lock-string-face) + (agda2-highlight-symbol-face . font-lock-variable-name-face) + (agda2-highlight-primitive-type-face . font-lock-type-face) + (agda2-highlight-bound-variable-face . font-lock-variable-name-face) + (agda2-highlight-inductive-constructor-face . font-lock-type-face) + (agda2-highlight-coinductive-constructor-face . font-lock-type-face) + (agda2-highlight-datatype-face . font-lock-type-face) + (agda2-highlight-field-face . font-lock-type-face) + (agda2-highlight-function-face . font-lock-function-name-face) + (agda2-highlight-module-face . font-lock-variable-name-face) + (agda2-highlight-postulate-face . font-lock-type-face) + (agda2-highlight-primitive-face . font-lock-type-face) + (agda2-highlight-macro-face . font-lock-function-name-face) + (agda2-highlight-record-face . font-lock-type-face) + (agda2-highlight-error-face . font-lock-warning-face)))) :config (map! :map agda2-mode-map :localleader From 57415658a012124e3c9804f5c9639a46b947733c Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Mon, 3 Sep 2018 16:00:40 +0200 Subject: [PATCH 7/9] More syntax highlighting --- modules/lang/agda/config.el | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el index ea753aec7..5ae19aca1 100644 --- a/modules/lang/agda/config.el +++ b/modules/lang/agda/config.el @@ -11,8 +11,7 @@ :mode "\\.agda\\'" :after agda-input :init - ;; fix syntax highlighting - ;; (taken from https://github.com/syl20bnr/spacemacs/blob/develop/layers/%2Blang/agda/packages.el) + ;; make syntax-highlighting more consistent with other major modes (progn (mapc (lambda (x) (add-to-list 'face-remapping-alist x)) @@ -32,7 +31,14 @@ (agda2-highlight-primitive-face . font-lock-type-face) (agda2-highlight-macro-face . font-lock-function-name-face) (agda2-highlight-record-face . font-lock-type-face) - (agda2-highlight-error-face . font-lock-warning-face)))) + (agda2-highlight-error-face . font-lock-warning-face) + (agda2-highlight-dotted-face . font-lock-variable-name-face) + (agda2-highlight-unsolved-meta-face . font-lock-warning-face) + (agda2-highlight-unsolved-constraint-face . font-lock-warning-face) + (agda2-highlight-termination-problem-face . font-lock-warning-face) + (agda2-highlight-positivity-problem-face . font-lock-warning-face) + (agda2-highlight-incomplete-pattern-face . font-lock-warning-face) + (agda2-highlight-typechecks-face . font-lock-warning-face)))) :config (map! :map agda2-mode-map :localleader From 818df0afe437cb64c6cd0d550f20805cec63ac96 Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Mon, 3 Sep 2018 16:11:08 +0200 Subject: [PATCH 8/9] More keybindings --- modules/lang/agda/config.el | 30 ++++++++++++++++++++++++------ 1 file changed, 24 insertions(+), 6 deletions(-) diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el index 5ae19aca1..dce22f3a0 100644 --- a/modules/lang/agda/config.el +++ b/modules/lang/agda/config.el @@ -41,9 +41,27 @@ (agda2-highlight-typechecks-face . font-lock-warning-face)))) :config (map! :map agda2-mode-map - :localleader - :n "l" #'agda2-load - :n "d" #'agda2-infer-type-maybe-toplevel - :n "o" #'agda2-module-contents-maybe-toplevel - :n "n" #'agda2-compute-normalised-maybe-toplevel)) - ;; TODO finish keybindings + :localleader + :n "?" #'agda2-show-goals + :n "." #'agda2-goal-and-context-and-inferred + :n "," #'agda2-goal-and-context + :n "=" #'agda2-show-constraints + :n "SPC" #'agda2-give + :n "a" #'agda2-auto + :n "c" #'agda2-make-case + :n "d" #'agda2-infer-type-maybe-toplevel + :n "e" #'agda2-show-context + :n "gG" #'agda2-go-back + :n "h" #'agda2-helper-function-type + :n "l" #'agda2-load + :n "n" #'agda2-compute-normalised-maybe-toplevel + :n "p" #'agda2-module-contents-maybe-toplevel + :n "r" #'agda2-refine + :n "s" #'agda2-solveAll + :n "t" #'agda2-goal-type + :n "w" #'agda2-why-in-scope-maybe-toplevel + :n "xc" #'agda2-compile + :n "xd" #'agda2-remove-annotations + :n "xh" #'agda2-display-implicit-arguments + :n "xq" #'agda2-quit + :n "xr" #'agda2-restart)) From c23fe02869d2a33866f2e89d64ad04373174b486 Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Fri, 21 Sep 2018 14:52:42 +0200 Subject: [PATCH 9/9] Remove syntax highlighting --- modules/lang/agda/config.el | 35 +++-------------------------------- 1 file changed, 3 insertions(+), 32 deletions(-) diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el index dce22f3a0..dc21ae25c 100644 --- a/modules/lang/agda/config.el +++ b/modules/lang/agda/config.el @@ -4,41 +4,12 @@ (when (executable-find "agda-mode") (file-name-directory (shell-command-to-string "agda-mode locate")))) -(def-package! agda-input +(def-package! agda2 + :when +agda-dir :load-path +agda-dir) (def-package! agda2-mode - :mode "\\.agda\\'" - :after agda-input - :init - ;; make syntax-highlighting more consistent with other major modes - (progn - (mapc - (lambda (x) (add-to-list 'face-remapping-alist x)) - '((agda2-highlight-keyword-face . font-lock-keyword-face) - (agda2-highlight-string-face . font-lock-string-face) - (agda2-highlight-number-face . font-lock-string-face) - (agda2-highlight-symbol-face . font-lock-variable-name-face) - (agda2-highlight-primitive-type-face . font-lock-type-face) - (agda2-highlight-bound-variable-face . font-lock-variable-name-face) - (agda2-highlight-inductive-constructor-face . font-lock-type-face) - (agda2-highlight-coinductive-constructor-face . font-lock-type-face) - (agda2-highlight-datatype-face . font-lock-type-face) - (agda2-highlight-field-face . font-lock-type-face) - (agda2-highlight-function-face . font-lock-function-name-face) - (agda2-highlight-module-face . font-lock-variable-name-face) - (agda2-highlight-postulate-face . font-lock-type-face) - (agda2-highlight-primitive-face . font-lock-type-face) - (agda2-highlight-macro-face . font-lock-function-name-face) - (agda2-highlight-record-face . font-lock-type-face) - (agda2-highlight-error-face . font-lock-warning-face) - (agda2-highlight-dotted-face . font-lock-variable-name-face) - (agda2-highlight-unsolved-meta-face . font-lock-warning-face) - (agda2-highlight-unsolved-constraint-face . font-lock-warning-face) - (agda2-highlight-termination-problem-face . font-lock-warning-face) - (agda2-highlight-positivity-problem-face . font-lock-warning-face) - (agda2-highlight-incomplete-pattern-face . font-lock-warning-face) - (agda2-highlight-typechecks-face . font-lock-warning-face)))) + :defer t :config (map! :map agda2-mode-map :localleader