~vonfry/dotfiles

780898278d9d2285bc10fec4254c0a0518a83999 — Vonfry 2 months ago 5f9a35b
emacs/agda & pg: modify some keybindings
M etc/nixos/modules/user/files/emacs.d/modules/lang/agda/packages.el => etc/nixos/modules/user/files/emacs.d/modules/lang/agda/packages.el +33 -29
@@ 7,40 7,44 @@
  (+agda--mode-load)
  :general
  (nmap-leader :keymaps 'agda2-mode-map
    "("   'agda2-infer-type-maybe-toplevel
    "&"   'agda2-search-about-toplevel
    ";"   'agda2-module-contents-maybe-toplevel
    ","   'agda2-go-back
    "."   'agda2-goto-definition-keyboard
    ","   'agda2-go-back
    ";"   'agda2-module-contents-maybe-toplevel
    "&"   'agda2-search-about-toplevel
    "r"   'agda2-compile
    "{"   'agda2-auto-maybe-all
    "} ." 'agda2-goal-and-context-and-inferred
    "} ;" 'agda2-goal-and-context-and-checked
    "} t" 'agda2-show-context
    "} r" 'agda2-solve-maybe-all
    "} {" 'agda2-show-goals
    "} n" 'agda2-next-goal
    "} p" 'agda2-previous-goal
    "} t" 'agda2-goal-type
    "} r" 'agda2-refine
    "} c" 'agda2-make-case
    "?"   'agda2-helper-function-type
    "t"   'agda2-goal-and-context
    "["   'agda2-why-in-scope-maybe-toplevel
    "("   'agda2-compute-normalised-maybe-toplevel
    ")"   'agda2-show-constraints
    ")"   'eri-indent
    "("   'eri-indent-reverse
    "c x" 'agda2-comment-dwim-rest-of-buffer
    "' b" 'agda2-load
    "r"   'agda2-compile

    "RET"   'agda2-give
    "' RET" 'agda2-elaborate-give)
  (nmap-mode :keymaps 'agda2-mode-map
    "q" 'agda2-quit
    "R" 'agda2-restart
    "A" 'agda2-abort
    "d" 'agda2-remove-annotations
    "h" 'agda2-display-implicit-arguments
    "i" 'agda2-display-irrelevant-arguments
    "S" 'agda2-set-program-version
    ")" 'eri-indent
    "(" 'eri-indent-reverse))
    "q"   'agda2-quit
    "R"   'agda2-restart
    "A"   'agda2-abort
    "d"   'agda2-remove-annotations
    "h"   'agda2-display-implicit-arguments
    "i"   'agda2-display-irrelevant-arguments
    "S"   'agda2-set-program-version
    "a"   'agda2-auto-maybe-all
    "d"   'agda2-infer-type-maybe-toplevel
    ","   'agda2-goal-and-context
    "."   'agda2-goal-and-context-and-inferred
    ";"   'agda2-goal-and-context-and-checked
    "e"   'agda2-show-context
    "s"   'agda2-solve-maybe-all
    "?"   'agda2-show-goals
    "n"   'agda2-next-goal
    "p"   'agda2-previous-goal
    "t"   'agda2-goal-type
    "r"   'agda2-refine
    "c"   'agda2-make-case
    "N"   'agda2-compute-normalised-maybe-toplevel
    ")"   'agda2-show-constraints
    "w"   'agda2-why-in-scope-maybe-toplevel
    "v"   'agda2-display-program-version
    "V"   'agda2-set-program-version
    "?"   'agda2-helper-function-type
    ))

M etc/nixos/modules/user/files/emacs.d/modules/lang/proof/packages.el => etc/nixos/modules/user/files/emacs.d/modules/lang/proof/packages.el +3 -2
@@ 4,20 4,21 @@
(use-package proof-general
  :general
  (nmap-leader :keymaps 'coq-mode-map
    "."      'proof-goto-point
    "\""     'proof-shell-start
    "' x"    'proof-shell-exit
    "' >"    'proof-autosend-toggle
    "' u"    'proof-undo-last-successful-command
    "' b"    'proof-process-buffer
    "&"      'proof-find-theorems
    "DEL"    'proof-undo-and-delete-last-successful-command
    "RET"    'proof-goto-point)
  (nmap-mode :keymaps 'coq-mode-map
    "b"      'proof-process-buffer
    "r"      'proof-retract-buffer
    "p"      'proof-prf
    "t"      'proof-ctxt
    "h"      'proof-help
    "`"      'proof-next-error
    "f"      'proof-find-theorems
    "v"      'proof-minibuffer-cmd
    "b"      'proof-toolbar-toggle
    "c"      'proof-interrupt-process