Improve emacs config.

emacs.d/init.el

@@ -6,8 +6,19 @@
 ;; need to know about Emacs (what commands exist, what functions do,
 ;; what variables specify), the help system can provide.
 
+;; Add the NonGNU ELPA package archive
+(require 'package)
+(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/"))
+(add-to-list 'package-archives  '("nongnu" . "https://elpa.nongnu.org/nongnu/"))
+
+;; Disable splash screen
+(setq inhibit-startup-screen t)
+
+;; Disable satanic torture
+(blink-cursor-mode 0)
+
 ;; Set default font face
-(set-face-attribute 'default nil :font "Fira Mono")
+(set-face-attribute 'default nil :font "Fira Mono" :height 125)
 
 ;; Disable the menu bar
 (menu-bar-mode -1)
@@ -18,9 +29,12 @@
 ;; Disable the scroll bars
 (scroll-bar-mode -1)
 
+(defun install-package-if-missing (pkg)
+  (unless (package-installed-p pkg)
+    (package-install pkg)))
+
 ;;; Completion framework
-(unless (package-installed-p 'vertico)
+(install-package-if-missing 'vertico)
-  (package-install 'vertico))
 
 ;; Enable completion by narrowing
 (vertico-mode t)
@@ -32,59 +46,58 @@
   (define-key vertico-map (kbd "M-d") #'vertico-directory-delete-char))
 
 ;;; Extended completion utilities
-(unless (package-installed-p 'consult)
+(install-package-if-missing 'consult)
-  (package-install 'consult))
 (global-set-key [rebind switch-to-buffer] #'consult-buffer)
 
 ;;; LSP Support
-(unless (package-installed-p 'eglot)
+(install-package-if-missing 'lsp-mode)
-  (package-install 'eglot))
-
-;; Enable LSP support by default in programming buffers
-(add-hook 'prog-mode-hook #'eglot-ensure)
 
 ;;; Pop-up auto-completion
-(unless (package-installed-p 'company)
+(install-package-if-missing 'company)
-  (package-install 'company))
 
 ;; Enable Company by default in programming buffers
 (add-hook 'prog-mode-hook #'company-mode)
 
 ;;; Indication of local VCS changes
-(unless (package-installed-p 'diff-hl)
+(install-package-if-missing 'diff-hl)
-  (package-install 'diff-hl))
 
 ;; Enable `diff-hl' support by default in programming buffers
 (add-hook 'prog-mode-hook #'diff-hl-mode)
 
+;;; Lean Support
+(let ((path "~/lean4-mode"))
+  (when (file-exists-p path)
+    (setq load-path (cons path load-path))
+    (dolist (p '(dash f flycheck lsp-mode magit-section s))
+      (install-package-if-missing p))
+    (require 'lean4-mode)))
+(setq lean4-highlight-inaccessible-names nil)
+
 ;;; Rust Support
-(unless (package-installed-p 'rust-mode)
+(install-package-if-missing 'rust-mode)
-  (package-install 'rust-mode))
 
 ;;; LaTeX support
-(unless (package-installed-p 'auctex)
+(install-package-if-missing 'auctex)
-  (package-install 'auctex))
 (setq TeX-auto-save t)
 (setq TeX-parse-self t)
 (setq-default TeX-master nil)
 
 ;;; Markdown support
-(unless (package-installed-p 'markdown-mode)
+(install-package-if-missing 'markdown-mode)
-  (package-install 'markdown-mode))
 
 ;;; EditorConfig support
-(unless (package-installed-p 'editorconfig)
+(install-package-if-missing 'editorconfig)
-  (package-install 'editorconfig))
-
-;; Enable EditorConfig
 (editorconfig-mode t)
 
 ;;; Vim Emulation
-(unless (package-installed-p 'evil)
+(install-package-if-missing 'evil)
-  (package-install 'evil))
-
-;; Enable Vim emulation
 (evil-mode t)
+(install-package-if-missing 'evil-commentary)
+(evil-commentary-mode)
+
+;;; Color Themes
+(install-package-if-missing 'color-theme-sanityinc-tomorrow)
+(load-theme 'sanityinc-tomorrow-bright t)
 
 ;; Miscellaneous options
 (setq-default major-mode