我打开 emacs,然后打开一个 .v 文件,以便触发 Proof General。但是,这样做的 IDE 非常慢,并且需要很长时间才能上下滚动证明。关于为什么会发生这种情况的任何想法?
配置文件:
;; use standard keys for undo cut copy paste
(cua-mode 1)
;; disable bell sound
(setq ring-bell-function 'ignore)
(defun proof-retract-buffer-stay ()
"Call proof-retract-buffer, but retain position"
(interactive)
(proof-retract-buffer nil)
)
;; keybindings for forward and backward Coq
;; disable C-c C-v from ProofGeneral
(eval-after-load "proof-script" '(progn
(define-key proof-mode-map (kbd "C-M-<down>") 'proof-assert-next-command-interactive)
(define-key proof-mode-map (kbd "C-M-<up>") 'proof-undo-last-successful-command)
(define-key proof-mode-map (kbd "C-M-<left>") 'proof-retract-buffer-stay)
(define-key proof-mode-map (kbd "C-M-<right>") 'proof-goto-point)
(define-key proof-mode-map (kbd "C-c C-v") nil)
(set-face-background 'proof-locked-face "#88D9FF")
))
(eval-after-load "coq" '(progn
(set-face-background 'coq-cheat-face "#ffe87a")
(set-face-foreground 'coq-cheat-face "#ff141d")
))
;; start maximized
(toggle-frame-maximized)
;; disable Proof General splash screen
(setq proof-splash-enable nil)
;; disable emacs splash screen
(setq inhibit-startup-screen t)
;; forces hybrid mode for displaying Coq buffers
(setq proof-three-window-mode-policy 'hybrid)
;; MELA repo
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
(package-initialize)
;; company-coq!
(add-hook 'coq-mode-hook #'company-coq-mode)
(setq company-coq-live-on-the-edge t)