Fix agda indentation and README
This commit is contained in:
parent
5096202b6b
commit
dbbdca7d5d
|
@ -34,10 +34,16 @@ Then check that =agda= is available on your =$PATH= and seen by Emacs. For
|
||||||
information about setting up =$PATH=, check out the corresponding section in the
|
information about setting up =$PATH=, check out the corresponding section in the
|
||||||
FAQ (~SPC h SPC $PATH RET~).
|
FAQ (~SPC h SPC $PATH RET~).
|
||||||
|
|
||||||
By default the =agda-mode= executable bundled with most agda installations
|
By default the =agda-mode= executable bundled with most agda installations is
|
||||||
is used to locate the agda-mode package. If you don't have it and want to use
|
used to locate the agda-mode package. If you don't have it and want to use a
|
||||||
a local agda-mode package, you can customize the layer variable =agda-mode-path=
|
local agda-mode package, you can customize the layer variable =agda-mode-path=
|
||||||
to your needs.
|
to your needs. Set it to =nil= if =agda2.el= is already discoverable in Emacs’
|
||||||
|
load path, otherwise set it to the path at which =agda2.el= can be found. For
|
||||||
|
example,
|
||||||
|
|
||||||
|
#+BEGIN_SRC emacs-lisp
|
||||||
|
(agda2 :variables agda-mode-path "/some/path/to/agda2.el")
|
||||||
|
#+END_SRC
|
||||||
|
|
||||||
* Key bindings
|
* Key bindings
|
||||||
The key bindings of this layer don't follow the Spacemacs conventions,
|
The key bindings of this layer don't follow the Spacemacs conventions,
|
||||||
|
|
|
@ -10,6 +10,7 @@
|
||||||
;;; License: GPLv3
|
;;; License: GPLv3
|
||||||
|
|
||||||
(defvar agda-mode-path 'use-helper
|
(defvar agda-mode-path 'use-helper
|
||||||
"Indicates the location of the agda-mode package.
|
"Indicates the location of the agda-mode package (the file
|
||||||
If `nil', it is assumed to be already available by Emacs.
|
`agda2.el') If `nil', it is assumed to be already available by
|
||||||
If `'use-helper', the `agda-mode' executable is used to find its location.")
|
Emacs. If `use-helper', the `agda-mode' executable is used to
|
||||||
|
find its location.")
|
||||||
|
|
|
@ -13,13 +13,16 @@
|
||||||
'((agda :location local)))
|
'((agda :location local)))
|
||||||
|
|
||||||
(defun agda/init-agda ()
|
(defun agda/init-agda ()
|
||||||
(if (and (eq agda-mode-path 'use-helper) (not (executable-find "agda-mode")))
|
(if (and (eq 'use-helper agda-mode-path)
|
||||||
|
(not (executable-find "agda-mode")))
|
||||||
(spacemacs-buffer/warning
|
(spacemacs-buffer/warning
|
||||||
(concat "Couldn't find `agda-mode', make sure it is "
|
(concat "Couldn't find `agda-mode', make sure it is "
|
||||||
"available in your PATH or check the installation "
|
"available in your PATH or check the installation "
|
||||||
"instructions in the README file."))
|
"instructions in the README file."))
|
||||||
|
|
||||||
(when (eq agda-mode-path 'use-helper) (setq agda-mode-path (let ((coding-system-for-read 'utf-8)) (shell-command-to-string "agda-mode locate"))))
|
(when (eq 'use-helper agda-mode-path)
|
||||||
|
(setq agda-mode-path (let ((coding-system-for-read 'utf-8))
|
||||||
|
(shell-command-to-string "agda-mode locate"))))
|
||||||
|
|
||||||
(use-package agda2-mode
|
(use-package agda2-mode
|
||||||
:defer t
|
:defer t
|
||||||
|
|
Loading…
Reference in a new issue