TakeV/spacemacs
Archived
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
This repository has been archived on 2024-10-22. You can view files and clone it, but cannot push or open issues or pull requests.
spacemacs/layers/+lang/agda/packages.el

102 lines
3.9 KiB
EmacsLisp
Raw Normal View History

Deprecation of extensions and <pkg>-excluded-packages variables As announced in previous releases, see CHANGELOG.next for more info in the Breaking Changes section.
2016-01-18 03:06:04 +00:00
;;; packages.el --- Agda2 Layer packages File for Spacemacs
lang/agda-mode: New layer
2015-04-14 20:55:13 +00:00
;;
Happy New Year 2018!
2018-01-04 07:00:25 +00:00
;; Copyright (c) 2012-2018 Sylvain Benner & Contributors
lang/agda-mode: New layer
2015-04-14 20:55:13 +00:00
;;
;; Author: Oliver Charles <ollie@ocharles.org.uk>
;; URL: https://github.com/syl20bnr/spacemacs
;;
;; This file is not part of GNU Emacs.
;;
;;; License: GPLv3
Fixed agda-post-packages -> agda-packages (develop)
2016-04-29 14:34:08 +00:00
(setq agda-packages
Unify packages list parentheses style problem: some layer packages lists have the open and closing parentheses on the same line as the first and last listed package, but most seem to have them on a separate lines. solution: put the open and close parentheses on separate lines, except for lists with only a single package, they are written on the same line as the variable name and parentheses. fix the lists indentation
2018-11-20 19:55:37 +00:00
'(
(agda :location local)
Enable auto-completion in Agda layer
2016-10-06 13:42:46 +00:00
company
Unify packages list parentheses style problem: some layer packages lists have the open and closing parentheses on the same line as the first and last listed package, but most seem to have them on a separate lines. solution: put the open and close parentheses on separate lines, except for lists with only a single package, they are written on the same line as the variable name and parentheses. fix the lists indentation
2018-11-20 19:55:37 +00:00
golden-ratio
))
lang/agda-mode: New layer
2015-04-14 20:55:13 +00:00
Enable auto-completion in Agda layer
2016-10-06 13:42:46 +00:00
(defun agda/post-init-company ()
Refactor and simplify company backends declaration Enabling a company backend for a specific mode was a tedious tasks with code scattered at different locations, one for local variable definitions, one for company hook function definitions and another where the backends were pushed to the local variables (which was problematic, since we ended up pushing the same backends over and over again with `SPC f e R`, pushes have been replaced by add-to-list calls in the new macro). All these steps are now put together at one place with the new macro spacemacs|add-company-backends, check its docstring for more info on its arguments. This macro also allows to define arbitrary buffer local variables to tune company for specific modes (similar to layer variables via a keyword :variables) The code related to company backends management has been moved to the auto-completion layer in the funcs.el file. A nice side effect of this move is that it enforces correct encapsulation of company backends related code. We can now easily detect if there is some configuration leakage when the auto-completion layer is not used. But we loose macro expansion at file loading time (not sue it is a big concern though). The function spacemacs|enable-auto-complete was never used so it has been deleted which led to the deletion of the now empty file core-auto-completion.el. The example in LAYERS.org regarding auto-completion is now out of date and has been deleted. An example to setup auto-completion is provided in the README.org file of the auto-completion layer.
2017-01-02 05:39:04 +00:00
(spacemacs|add-company-backends :backends company-capf :modes agda2-mode))
Enable auto-completion in Agda layer
2016-10-06 13:42:46 +00:00
lang/agda-mode: New layer
2015-04-14 20:55:13 +00:00
(defun agda/init-agda ()
Fix agda indentation and README
2016-08-17 18:20:20 +00:00
(if (and (eq 'use-helper agda-mode-path)
(not (executable-find "agda-mode")))
(spacemacs-buffer/warning
(concat "Couldn't find `agda-mode', make sure it is "
"available in your PATH or check the installation "
"instructions in the README file."))
lang/agda-mode: New layer
2015-04-14 20:55:13 +00:00
Fix agda indentation and README
2016-08-17 18:20:20 +00:00
(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"))))
lang/agda-mode: New layer
2015-04-14 20:55:13 +00:00
Adapt agda2-auto call to agda 2.6.0 changes * It's now agda2-auto-maybe-all. If you are not currently in a hole it tries to `auto` all holes by default. * Find and set an agda-version variable, to keep compatibility with previous agda versions.
2019-05-21 11:40:39 +00:00
(progn
(setq agda-version-out (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda --version")))
(string-match "\\([0-9]+\\.\\)*[0-9]+" agda-version-out)
(setq agda-version (match-string 0 agda-version-out)))
(setq agda2-auto (if (string< agda-version "2.6.0")
'agda2-auto
'agda2-auto-maybe-all))
Fix Agda layer for users without 'agda-mode' executable.
2016-08-06 20:36:11 +00:00
(use-package agda2-mode
Revert "Defer packages by default using use-package-always-defer" This reverts commit 29c78ce841ee5a99bb4077a2862afc96c8136107 and all other fixes that have been made afterwards. The motivation is that use-package is seen by many as a replacement for `require`. Is use-package always defer the loading of packages then is breaks this use case, this does not respect POLA so even if it was making Spacemacs loading faster (up to 3s faster on some startup on my machine) we just cannot use it, it would be irresponsible. Spacemacs should be easy to use, loading performance will come with time but it is not a priority.
2018-03-04 04:37:53 +00:00
:defer t
Fix Agda layer for users without 'agda-mode' executable.
2016-08-06 20:36:11 +00:00
:init (when agda-mode-path (load-file agda-mode-path))
Refactor jump to definition This commit defines: - spacemacs-default-jump-handlers: a list of functions that can jump to definition in ALL modes. - spacemacs-jump-handlers-MODE: a list of functions that can jump to definition in MODE. - spacemacs-jump-handlers: a buffer-local list of functions that can jump to definition. This is made up of the values of the two previous variables whenever a given major mode is activated. - spacemacs/jump-to-definition: a function that tries each function in spacemacs-jump-handlers in order, and stops when one of them takes us somewhere new. - spacemacs|define-jump-handlers: a macro that * defines spacemacs-jump-handlers-MODE, possibly filled with initial functions * defines a function that is added to the hook of the given MODE * binds “SPC m g g” of that MODE to spacemacs/jump-to-definition This is an attempt to harmonize all the different approaches to jumping. Specifically, - Existing intelligent jump packages that work for only a single mode should go to the beginning of spacemacs-jump-handlers-MODE. E.g. anaconda for python, ensime for scala, etc. - Packages like gtags that work for several modes (but potentially not all) and which is dumber than the intelligent jumpers should go the the END of spacemacs-jump-handlers-MODE. - Packages like dumb-jump that work for all modes should go to spacemacs-default-jump-handlers. In all cases the order of the jump handlers in each list should be from most to least intelligent. Fixes #6619
2016-08-13 13:43:37 +00:00
(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))))
Fix Agda layer for users without 'agda-mode' executable.
2016-08-06 20:36:11 +00:00
:config
(progn
(spacemacs|define-transient-state goal-navigation
:title "Goal Navigation Transient State"
:doc "\n[_f_] next [_b_] previous [_q_] quit"
:bindings
("f" agda2-next-goal)
("b" agda2-previous-goal)
("q" nil :exit t))
(spacemacs/set-leader-keys-for-major-mode 'agda2-mode
"f" 'spacemacs/goal-navigation-transient-state/agda2-next-goal
"b" 'spacemacs/goal-navigation-transient-state/agda2-previous-goal)
agda layer: refactor layer to use `use-package` - display a warning if agda has not been found - add a micro-state to easily navigate between the goals - use face-remapping-alist to redefine the faces - add some missing key bindings - add support for golden-ratio - add quick cabal instruction to install agda - sort key bindings alphabetically
2015-05-18 05:51:03 +00:00
Fix Agda layer for users without 'agda-mode' executable.
2016-08-06 20:36:11 +00:00
(spacemacs/set-leader-keys-for-major-mode 'agda2-mode
"?" 'agda2-show-goals
"." 'agda2-goal-and-context-and-inferred
"," 'agda2-goal-and-context
"=" 'agda2-show-constraints
"SPC" 'agda2-give
Adapt agda2-auto call to agda 2.6.0 changes * It's now agda2-auto-maybe-all. If you are not currently in a hole it tries to `auto` all holes by default. * Find and set an agda-version variable, to keep compatibility with previous agda versions.
2019-05-21 11:40:39 +00:00
"a" agda2-auto
Fix Agda layer for users without 'agda-mode' executable.
2016-08-06 20:36:11 +00:00
"c" 'agda2-make-case
"d" 'agda2-infer-type-maybe-toplevel
"e" 'agda2-show-context
"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
"xc" 'agda2-compile
"xd" 'agda2-remove-annotations
"xh" 'agda2-display-implicit-arguments
"xq" 'agda2-quit
Extract golden-ratio config to package fns
2016-08-18 19:10:43 +00:00
"xr" 'agda2-restart)))))
Fix Agda layer for users without 'agda-mode' executable.
2016-08-06 20:36:11 +00:00
Fix typo in Agda's packages.el
2016-11-14 12:22:16 +00:00
(defun agda/pre-init-golden-ratio ()
Extract golden-ratio config to package fns
2016-08-18 19:10:43 +00:00
(spacemacs|use-package-add-hook golden-ratio
:post-config
(add-to-list 'golden-ratio-exclude-buffer-names
"*Agda information*")))
Reference in a new issue Copy permalink