Commit graph

11 commits

Author SHA1 Message Date
Boris Buliga
d81e75584e
bump year in the copyright headers
Folks, this time of year has come. We can bump year in the copyright headers.
Let's celebrate!
2018-10-16 20:27:05 +03:00
Jeremy Bi
955b2a19d6 proof-general is added in MELPA 2018-09-03 20:18:28 +01:00
Langston Barrett
8fcf41cd54 coq: add keybindings for company-coq's documentation functions 2018-08-20 22:42:23 +01:00
Langston Barrett
178b0caeb8 lang/coq: more insertion keybindings 2018-08-09 22:49:01 +01:00
syl20bnr
ebe4c60264 Revert "Defer packages by default using use-package-always-defer"
This reverts commit 29c78ce841 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-03 23:40:10 -05:00
syl20bnr
29c78ce841 Defer packages by default using use-package-always-defer
Warning now `:defer t` is implied, to force a package to load `:demand t` is
now necessary.
2018-02-27 23:32:52 -05:00
Eivind Fonn
f4b53d2a4f Rename :depends to :requires 2017-07-03 09:54:53 +02:00
Eivind Fonn
08561d8631 core: implement :depends for package declarations
This replaces the older pattern
:toggle (configuration-layer/package-usedp ..)

This implementation ensures that :disabled-for honors dependent packages, i.e.
if package a depends on package b, which is owned by layer c, and layer c is
disabled for layer d, then neither package a nor b will be configured for layer
d. Previously, this was only true for package a, but not b.

This commit also fixes:

- configuration-layer/describe-package now shows which post-init and pre-init
  functions are disabled, if any
- Does not recreate all layer objects unconditionally when calling
  configuration-layer/discover-layers. Previously, this led to all layers being
  recreated after e.g. `SPC h SPC`, without any of the dotfile information.
  Since this information is now necessary for
  configuration-layer/describe-package, it’s important that we don’t clear the
  indexed layers when invoking this function.
2017-06-22 11:53:05 +02:00
syl20bnr
8f1a5d6fd5 coq: fix some configuration
- delete some diminish expressions which are not related to PG and user
  spacemacs|hide-lighter instead of spacemacs|diminish
- move company related configuration to the correct place
- move setq expressions to :init blocks to allow users to easily change them
2017-02-12 23:45:56 -05:00
syl20bnr
fe168f07b3 coq: update key bindings and README
README:
- add `SPC m` prefixes to follow the style of the other READMEs
- Sort key bindings alphabetically

Key bindings changes made to be more mnemocnic and/or to better fit the other
key bindings of other layers:

- SPC m p b --> SPC m p p (show prover process buffer)
- SPC m p c --> SPC m p i (interrupt prover process)
- SPC m p x --> SPC m p q (quit prover process, maybe SPC m p k for kill would
  be better ?)

- SPC m a p --> SPC m a a to print query
- SPC m a n p --> SPC m a A to print query showing all
- SPC m a i p --> SPC m a i i to print query showing implicits
- Ask showing all bindings use the same keys as regular Ask but the last key
  is capitalized, example: SPC m a b (ask about) and SPC m a B (ask about
  showing all)
- Ask showing implicits are still on SPC m a i (we could also use Control key,
  for instance SPC m a b (ask about) and SPC m a C-b (ask about show implicit),
  it depends on how frequent showing implicits are used).

- SPC m g . --> SPC m g l (go to end of Locked command)
- SPC m g d --> SPC m g g (using the jump handlers facility of Spacemacs)
- SPC m g a --> SPC m g s (to go to start of command)
2017-02-12 22:24:25 -05:00
Jeremy Bi
8b72130fc5 Add coq layer 2017-02-12 21:31:44 -05:00