I open emacs and then a .v file so that Proof General is triggered. However, one this is done the IDE is very slow and it takes ages to scroll up and down the proof. Any idea on why this might be happening?
Configuration file:
;; 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)