Agda .emacs

.emacs

(add-to-list 'load-path "~/.emacs.d/evil")
(require 'evil)
(evil-mode 1)

;; Highlight matching parens.
(show-paren-mode 1)

;;; No tabs.
(setq-default ident-tabs-mode nil)
(setq-default tab-width 4)

;;; Hidden scroll.
;;; Hidden toolbar.
(if (display-graphic-p)
    (progn
      (tool-bar-mode -1)
      (scroll-bar-mode -1)
      (menu-bar-mode -1)))

;;; Disable blinking cursor.
(blink-cursor-mode 0)

;;; Disable bell.
(setq ring-bell-function 'ignore)

;;; Show trailing whitespace, long lines, etc.
(require 'whitespace)
(setq whitespace-style '(face empty tabs lines-tail trailing))
; ; (setq whitespace-line-column 79)
(global-whitespace-mode t)

;;; Haskell mode.
; (add-to-list 'load-path "~/.emacs.d/haskell-mode/")
; (require 'haskell-mode-autoloads)
; (add-to-list 'Info-default-directory-list "~/emacs.d/haskell-mode/")
; (add-hook 'haskell-mode-hook 'turn-on-haskell-doc-mode)
; (add-hook 'haskell-mode-hook 'turn-on-haskell-indentation)

;;; Agda mode.
(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

; (package-initialize)
; (exec-path-from-shell-initialize)

; (let ((base03    "#1c1c1c")
;       (base02    "#262626")
;       (base01    "#4e4e4e")
;       (base00    "#585858")
;       (base0     "#808080")
;       (base1     "#8a8a8a")
;       (base2     "#d7d7af")
;       (base3     "#ffffd7")
;       (yellow    "#af8700")
;       (orange    "#d75f00")
;       (red       "#d70000")
;       (magenta   "#af005f")
;       (violet    "#5f5faf")
;       (blue      "#0087ff")
;       (cyan      "#00afaf")
;       (green     "#5f8700"))
;     (custom-set-faces
;      `(agda2-highlight-keyword-face ((t (:foreground ,orange))))
;      `(agda2-highlight-string-face ((t (:foreground ,magenta))))
;      `(agda2-highlight-number-face ((t (:foreground ,violet))))
;      ; `(agda2-highlight-symbol-face ((((background ,base3)) (:foreground ,base01))))
;      `(agda2-highlight-symbol-face ((((background ,base3)) (:foreground ,base0))))
;      `(agda2-highlight-primitive-type-face ((t (:foreground ,blue))))
;      `(agda2-highlight-bound-variable-face ((t nil)))
;      `(agda2-highlight-inductive-constructor-face ((t (:foreground ,green))))
;      `(agda2-highlight-coinductive-constructor-face ((t (:foreground ,yellow))))
;      `(agda2-highlight-datatype-face ((t (:foreground ,blue))))
;      `(agda2-highlight-field-face ((t (:foreground ,red))))
;      `(agda2-highlight-function-face ((t (:foreground ,blue))))
;      `(agda2-highlight-module-face ((t (:foreground ,violet))))
;      `(agda2-highlight-postulate-face ((t (:foreground ,blue))))
;      `(agda2-highlight-primitive-face ((t (:foreground ,blue))))
;      `(agda2-highlight-record-face ((t (:foreground ,blue))))
;      `(agda2-highlight-dotted-face ((t nil)))
;      `(agda2-highlight-operator-face ((t nil)))
;      `(agda2-highlight-error-face ((t (:foreground ,red :underline t))))
;      `(agda2-highlight-unsolved-meta-face ((t (:background ,base03 :foreground ,yellow))))
;      `(agda2-highlight-unsolved-constraint-face ((t (:background ,base03 :foreground ,yellow))))
;      `(agda2-highlight-termination-problem-face ((t (:background ,orange :foreground ,base03))))
;      `(agda2-highlight-incomplete-pattern-face ((t (:background ,orange :foreground ,base03))))
;      `(agda2-highlight-typechecks-face ((t (:background ,cyan :foreground ,base03))))))

; http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VIMEditing
;;; Maps C-c C-<key> to \<key in evil-normal-state
; Original mappigns (more):
; https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda2-mode.el#L223

; Simplify the goal and context.
(defun goal-and-context-normalized ()
  (interactive)
  (agda2-goal-and-context '(16)))

(defun goal-and-context-and-inferred-normalized ()
  (interactive)
  (agda2-goal-and-context-and-inferred '(16)))

(eval-after-load 'agda2
  '(progn
      (evil-define-key 'normal agda2-mode-map
	"\\a" 'agda2-auto
	"\\k" 'agda2-previous-goal
	"\\j" 'agda2-next-goal
	"\\c" 'agda2-make-case
	"\\d" 'agda2-infer-type-maybe-toplevel
	"\\e" 'agda2-show-context
	"\\h" 'agda2-helper-function-type
	"\\l" 'agda2-load
	"\\n" 'agda2-compute-normalised-maybe-toplevel
	"\\o" 'agda2-module-contents-maybe-toplevel
	"\\r" 'agda2-refine
	"\\s" 'agda2-solveAll
	"\\t" 'agda2-goal-type
	"\\ " 'agda2-give
	"\\<" 'goal-and-context-normalized
	"\\," 'agda2-goal-and-context
	"\\>" 'goal-and-context-and-inferred-normalized
	"\\." 'agda2-goal-and-context-and-inferred
	"\\=" 'agda2-show-constraints
	"\\?" 'agda2-show-goals
	"\\xc" 'agda2-compile
	"\\xd" 'agda2-remove-annotations
	"\\xh" 'agda2-display-implicit-arguments
	"\\xl" 'agda2-load
	"\\xq" 'agda2-quit
	"\\xr" 'agda2-restart)))