;; -*- lexical-binding: t; -*- (setq user-full-name "Yann Herklotz") (setq user-mail-address "yann@yannherklotz.com") (setq gc-cons-threshold (* 1024 1024 1024)) (global-set-key (kbd "M-u") #'upcase-dwim) (global-set-key (kbd "M-l") #'downcase-dwim) (global-set-key (kbd "M-c") #'capitalize-dwim) (global-set-key (kbd "C-c z") #'quick-calc) (global-set-key (kbd "") #'revert-buffer) (global-set-key (kbd "C-.") #'other-window) (global-set-key (kbd "C-,") #'ymhg/prev-window) (global-set-key (kbd "C-\\") #'undo-only) (global-set-key (kbd "M-SPC") (lambda () (interactive) (insert " "))) (global-set-key (kbd "C-") #'tab-bar-switch-to-recent-tab) (global-set-key (kbd "C-c l") #'org-store-link) (global-set-key (kbd "C-c c") #'org-capture) (define-prefix-command 'ymh-map) (global-set-key (kbd "C-c y") 'ymh-map) (define-key ymh-map (kbd "o") #'ymhg/reset-coq-windows) (define-key ymh-map (kbd "c") #'calendar) (define-key ymh-map (kbd "C-l") #'org-agenda-open-link) (define-key ymh-map (kbd "C-p") #'org-previous-link) (define-key ymh-map (kbd "C-n") #'org-next-link) ;;(define-key y-map (kbd "C-g") #'org-zettelkasten-goto-id) (set-register ?l (cons 'file "~/.emacs.d/loader.org")) (set-register ?m (cons 'file "~/Dropbox/org/meetings.org")) (set-register ?i (cons 'file "~/Dropbox/org/inbox.org")) (set-register ?p (cons 'file "~/Dropbox/org/projects.org")) (set-register ?c (cons 'file (format-time-string "~/Dropbox/org/%Y-%m.org"))) (defvar bootstrap-version) (let ((bootstrap-file (expand-file-name "straight/repos/straight.el/bootstrap.el" user-emacs-directory)) (bootstrap-version 6)) (unless (file-exists-p bootstrap-file) (with-current-buffer (url-retrieve-synchronously "https://raw.githubusercontent.com/radian-software/straight.el/develop/install.el" 'silent 'inhibit-cookies) (goto-char (point-max)) (eval-print-last-sexp))) (load bootstrap-file nil 'nomessage)) (setq straight-use-package-by-default t) (straight-use-package 'use-package) (use-package ymh-common :straight nil :load-path "ymh-emacs") (use-package emacs :straight nil :init (setq gnus-init-file (concat user-emacs-directory "gnus.el")) (setq-default fill-column 80) (setq completion-cycle-threshold 3) (setq tab-always-indent 'complete) (setq use-short-answers t) (setq inhibit-startup-message t) (setq confirm-nonexistent-file-or-buffer nil) (setq ring-bell-function 'ignore) (setq sentence-end-double-space t) (setq truncate-partial-width-windows nil) (setq-default bidi-paragraph-direction 'left-to-right) (if (version<= "27.1" emacs-version) (setq bidi-inhibit-bpa t)) ;; Set up dictionaries (setq read-extended-command-predicate #'command-completion-default-include-p) (setq enable-recursive-minibuffers t) (setq face-remapping-alist '((proof-locked-face . region))) (defvar --backup-directory) (setq --backup-directory (concat user-emacs-directory "backups")) (if (not (file-exists-p --backup-directory)) (make-directory --backup-directory t)) (setq backup-directory-alist `(("." . ,--backup-directory))) (setq make-backup-files t ; backup of a file the first time it is saved. backup-by-copying t ; don't clobber symlinks version-control t ; version numbers for backup files delete-old-versions t ; delete excess backup files silently delete-by-moving-to-trash t kept-old-versions 6 ; oldest versions to keep when a new numbered backup is made (default: 2) kept-new-versions 9 ; newest versions to keep when a new numbered backup is made (default: 2) auto-save-default t ; auto-save every buffer that visits a file auto-save-timeout 20 ; number of seconds idle time before auto-save (default: 30) auto-save-interval 200 ; number of keystrokes between auto-saves (default: 300) ) (setq vc-follow-symlinks t) (setq-default indent-tabs-mode nil) (setq-default tab-width 4) (setq-default python-indent-offset 4) (setq-default c-basic-offset 4) (setq line-number-display-limit 2000000) (setq default-frame-alist '((undecorated . t) (drag-internal-border . 1) (internal-border-width . 5))) (setq auth-sources '("~/.authinfo" "~/.authinfo.gpg" "~/.netrc")) (setq wdired-allow-to-change-permissions t) (add-hook 'text-mode-hook #'visual-line-mode) :config (unless (string= system-type "darwin") (menu-bar-mode -1)) (tool-bar-mode -1) (scroll-bar-mode -1) ;; Enable those (dolist (c '(overwrite-mode narrow-to-region narrow-to-page upcase-region downcase-region)) (put c 'disabled nil)) (set-face-attribute 'default nil :font "Iosevka YMHG Medium-12") (setq auto-mode-alist (append (list ;;'("\\.\\(vcf\\|gpg\\)\\'" . sensitive-minor-mode) '("\\.v\\'" . coq-mode) '("\\.sv\\'" . verilog-mode) '("\\.mkiv\\'" . context-mode) '("\\.mkii\\'" . context-mode) '("\\.mkxl\\'" . context-mode)) auto-mode-alist)) ;; Mac configuration (when (eq system-type 'darwin) (progn (setq mac-right-option-modifier 'none mac-command-modifier 'meta mac-option-modifier nil) (add-hook 'ns-system-appearance-change-functions #'ymhg/apply-theme)))) (use-package ymh-diary :straight nil :load-path "ymh-emacs") (use-package shr :straight nil :init (setq shr-use-fonts nil) (setq shr-max-image-proportion 0.5)) (use-package browse-url :straight nil :init (setq browse-url-handlers '(("wikipedia\\.org" . eww-browse-url) ("yannherklotz\\.com" . eww-browse-url) ("ymhg\\.org" . eww-browse-url) ("archlinux\\.org" . eww-browse-url) ("sachachua\\.com" . eww-browse-url) ("comonad\\.com" . eww-browse-url) ("drewdevault\\.com" . eww-browse-url) ("wordpress\\.com" . eww-browse-url) ("mathbabe\\.org" . eww-browse-url) ("ethz\\.ch" . eww-browse-url) ("pragmaticemacs\\.com" . eww-browse-url)))) (use-package message :straight nil :init (setq message-send-mail-function 'message-send-mail-with-sendmail) (setq message-fill-column 80) (setq message-signature "Yann Herklotz Imperial College London https://yannherklotz.com")) (use-package ispell :straight nil :init (setq ispell-dictionary "british")) (use-package delight :config (delight 'auto-revert-mode nil "autorevert") (delight 'eldoc-mode nil "eldoc")) (use-package project :straight nil :init (setq project-switch-commands '((project-find-file "Find file") (project-find-regexp "Find regexp") (project-find-dir "Find directory") (project-vc-dir "VC-Dir") (magit-project-status "Magit") (project-eshell "Eshell"))) :config (define-key project-prefix-map "m" #'magit-project-status)) (use-package tab-bar :straight nil :init (setq tab-bar-show nil) (setq tab-bar-select-tab-modifiers '(meta)) :config (tab-bar-mode 1)) (use-package flyspell :config (unbind-key "C-." flyspell-mode-map) (unbind-key "C-," flyspell-mode-map) (setq flyspell-mouse-map (make-sparse-keymap))) (use-package calc-forms :straight nil :config (add-to-list 'math-tzone-names '("AOE" 12 0)) (add-to-list 'math-tzone-names '("IST" (float -55 -1) 0))) (use-package calendar :straight nil :config (setq calendar-mark-diary-entries-flag t) (setq calendar-mark-holidays-flag t) (setq calendar-mode-line-format nil) (setq calendar-time-display-form '(24-hours ":" minutes (when time-zone (format "(%s)" time-zone)))) (setq calendar-week-start-day 1) ; Monday (setq calendar-date-style 'iso) (setq calendar-date-display-form calendar-iso-date-display-form) (setq calendar-time-zone-style 'numeric) ; Emacs 28.1 (add-hook 'calendar-today-visible-hook #'calendar-mark-today) (remove-hook 'calendar-mode-hook #'org--setup-calendar-bindings) (let ((map calendar-mode-map)) (define-key map (kbd "s") #'calendar-sunrise-sunset) (define-key map (kbd "l") #'lunar-phases) (define-key map (kbd "i") nil) ; Org sets this, much to my chagrin (see `remove-hook' above) (define-key map (kbd "i a") #'diary-insert-anniversary-entry) (define-key map (kbd "i c") #'diary-insert-cyclic-entry) (define-key map (kbd "i d") #'diary-insert-entry) ; for current "day" (define-key map (kbd "i m") #'diary-insert-monthly-entry) (define-key map (kbd "i w") #'diary-insert-weekly-entry) (define-key map (kbd "i y") #'diary-insert-yearly-entry) (define-key map (kbd "M-n") #'calendar-forward-month) (define-key map (kbd "M-p") #'calendar-backward-month))) (use-package cal-dst :straight nil :config (setq calendar-standard-time-zone-name "+0000") (setq calendar-daylight-time-zone-name "+0100")) (use-package diary-lib :straight nil :config (setq diary-file "~/Dropbox/org/diary") (setq diary-date-forms diary-iso-date-forms) (setq diary-comment-start ";;") (setq diary-comment-end "") (setq diary-nonmarking-symbol "!") (setq diary-show-holidays-flag t) (setq diary-display-function #'diary-fancy-display) ; better than its alternative (setq diary-header-line-format nil) (setq diary-list-include-blanks nil) (setq diary-number-of-entries 2) (setq diary-mail-days 2) (setq diary-abbreviated-year-flag nil) ;;(add-hook 'diary-list-entries-hook #'diary-fix-timezone t) (add-hook 'diary-list-entries-hook #'diary-sort-entries t) (add-hook 'diary-list-entries-hook 'diary-include-other-diary-files) (add-hook 'diary-mark-entries-hook 'diary-mark-included-diary-files)) (use-package appt :straight nil :init (setq appt-display-diary nil) (setq appt-disp-window-function #'appt-disp-window) (setq appt-display-mode-line t) (setq appt-display-interval 3) (setq appt-audible nil) (setq appt-warning-time-regexp "appt \\([0-9]+\\)") (setq appt-message-warning-time 15) :config (run-at-time 10 nil #'appt-activate 1)) (use-package savehist :straight nil :init (savehist-mode)) (use-package ef-themes :config (load-theme 'ef-dark t)) (use-package modus-themes :config ;;(load-theme 'modus-vivendi t) ) (use-package pass :bind (:map ymh-map ("q" . password-store-otp-token-copy) ("p" . password-store-copy) ("i" . password-store-insert) ("g" . password-store-generate))) (use-package magit) (use-package org :init (setq org-startup-indented nil) (setq org-src-window-setup 'current-window) (setq org-return-follows-link t) (setq org-confirm-babel-evaluate nil) (setq org-use-speed-commands t) (setq org-hide-emphasis-markers nil) (setq org-adapt-indentation nil) (setq org-cycle-separator-lines 2) (setq org-startup-folded 'content) (setq org-structure-template-alist '(("a" . "export ascii") ("c" . "center") ("C" . "comment") ("e" . "example") ("E" . "export") ("h" . "export html") ("l" . "export latex") ("q" . "quote") ("s" . "src") ("v" . "verse") ("el" . "src emacs-lisp") ("d" . "definition") ("t" . "theorem"))) (setq org-attach-auto-tag "attach") (setq org-reverse-note-order t) (setq org-fast-tag-selection-single-key 'expert) (setq org-log-done 'time) (setq org-log-into-drawer t) (setq org-icalendar-include-todo t) (setq org-icalendar-include-bbdb-anniversaries t) (setq org-refile-targets `(("~/Dropbox/org/main.org" :level . 1) ("~/Dropbox/org/someday.org" :level . 1) ("~/Dropbox/org/projects.org" :maxlevel . 2) (,(format-time-string "~/Dropbox/org/%Y-%m.org") :level . 1))) (setq org-todo-keywords '((sequence "TODO(t)" ; A task that needs doing & is ready to do "PROJ(p)" ; A project, which usually contains other tasks "STRT(s)" ; A task that is in progress "WAIT(w)" ; Something external is holding up this task "HOLD(h)" ; This task is paused/on hold because of me "DELG(l)" ; This task is delegated "SMDY(m)" ; todo some day "|" "DONE(d!)" ; Task successfully completed "KILL(k)") ; Task was cancelled, aborted or is no longer applicable (sequence "[ ](T)" ; A task that needs doing "[-](S)" ; Task is in progress "[?](W)" ; Task is being held up or paused "|" "[X](D)"))) (setq org-todo-keyword-faces '(("[-]" . "yellow") ("STRT" . (:background "aquamarine")) ("[?]" . (:weight bold)) ("WAIT" . "yellow") ("HOLD" . "yellow") ("DELG" . "goldenrod") ("SMDY" . "cadet blue") ("PROJ" . (:background "sea green" :weight bold)) ("NO" . (:background "dark salmon")) ("KILL" . "pale green"))) (setq org-html-head-include-default-style nil) (setq org-html-head-include-scripts nil) (setq org-html-doctype "html5") (setq org-html-html5-fancy t) (setq org-html-container-element "section") (setq org-html-postamble-format '(("en" ""))) (setq org-html-postamble t) (setq org-html-divs '((preamble "header" "header") (content "article" "content") (postamble "footer" "postamble"))) (setq org-export-with-broken-links t) :config (unbind-key "C-," org-mode-map)) (use-package org-agenda :straight nil :bind ("C-c a" . org-agenda) :init (setq org-agenda-files (mapcar 'expand-file-name (list "~/Dropbox/org/inbox.org" "~/Dropbox/org/main.org" "~/Dropbox/org/tickler.org" "~/Dropbox/org/projects.org" (format-time-string "~/Dropbox/org/%Y-%m.org") "~/Dropbox/bibliography/reading_list.org"))) (setq org-agenda-custom-commands '(("w" "At work" tags-todo "@work" ((org-agenda-overriding-header "Work"))) ("h" "At home" tags-todo "@home" ((org-agenda-overriding-header "Home"))) ("u" "At uni" tags-todo "@uni" ((org-agenda-overriding-header "University"))))) (setq org-agenda-tag-filter '("-backed")) (setq org-agenda-span 7) (setq org-agenda-start-day ".") (setq org-agenda-start-on-weekday nil) (setq org-agenda-include-diary t) (setq org-agenda-skip-deadline-if-done t) (setq org-agenda-skip-scheduled-if-done t) (setq org-agenda-show-all-dates t)) (use-package org-capture :straight nil :bind ("C-c c" . org-capture) :init (setq org-capture-templates `(("t" "Todo" entry (file "inbox.org") "* TODO %? :PROPERTIES: :ID: %(org-id-uuid) :END: :LOGBOOK: - State \"TODO\" from \"\" %U :END:" :empty-lines 1) ("l" "Link Todo" entry (file "inbox.org") "* TODO %? :PROPERTIES: :ID: %(org-id-uuid) :END: :LOGBOOK: - State \"TODO\" from \"\" %U :END: %a" :empty-lines 1) ("c" "Contacts" entry (file "~/Dropbox/org/contacts.org") "* %(org-contacts-template-name) :PROPERTIES: :EMAIL: %(org-contacts-template-email) :END:" :empty-lines 1)))) (use-package org-habit :straight nil) (use-package org-crypt :straight nil :after org :config (org-crypt-use-before-save-magic) (setq org-tags-exclude-from-inheritance '("crypt")) (setq org-crypt-key "8CEF4104683551E8")) (use-package org-id :straight nil :after org :config (setq org-id-link-to-org-use-id 'use-existing) (setq org-id-track-globally t)) (use-package org-transclusion :after org :config (setq org-transclusion-exclude-elements nil)) (use-package org-zettelkasten :after org :init (setq org-zettelkasten-directory "~/Dropbox/zk") :config (defun org-zettelkasten-goto-id (id) "Go to an ID." (interactive "sID: #") (cond ((string-prefix-p "1" id) (org-link-open-from-string (concat "[[file:" org-zettelkasten-directory "/hls.org::#" id "]]"))) ((string-prefix-p "2" id) (org-link-open-from-string (concat "[[file:" org-zettelkasten-directory "/computing.org::#" id "]]"))) ((string-prefix-p "3" id) (org-link-open-from-string (concat "[[file:" org-zettelkasten-directory "/verification.org::#" id "]]"))) ((string-prefix-p "4" id) (org-link-open-from-string (concat "[[file:" org-zettelkasten-directory "/mathematics.org::#" id "]]"))) ((string-prefix-p "5" id) (org-link-open-from-string (concat "[[file:" org-zettelkasten-directory "/hardware.org::#" id "]]"))))) (define-key ymh-map (kbd "C-g") #'org-zettelkasten-goto-id) (define-key ymh-map (kbd "s") (lambda () (interactive) (let ((org-agenda-files '("~/Dropbox/zk/hls.org" "~/Dropbox/zk/computing.org" "~/Dropbox/zk/verification.org" "~/Dropbox/zk/mathematics.org" "~/Dropbox/zk/hardware.org"))) (org-search-view)))) (add-hook 'org-mode-hook #'org-zettelkasten-mode)) (use-package pdf-tools :config (pdf-tools-install)) (use-package flycheck :delight flycheck-mode) (use-package rst) (use-package boogie-friends :config (setq flycheck-dafny-executable (executable-find "dafny")) (setq dafny-verification-backend 'cli)) (use-package direnv :config (direnv-mode)) (use-package orderless :init (setq completion-styles '(substring orderless basic))) (use-package vertico :init (setq read-file-name-completion-ignore-case t) (setq read-buffer-completion-ignore-case t) (setq completion-ignore-case t) (setq completion-category-defaults nil) (vertico-mode)) (use-package corfu :init (global-corfu-mode)) (use-package consult :bind (("M-s r" . consult-ripgrep) ("M-s g" . consult-git-grep) ("C-h a" . consult-apropos) ("M-s m" . consult-man) ("M-s h" . consult-org-heading))) (use-package dabbrev :straight nil ;; Swap M-/ and C-M-/ :bind (("M-/" . dabbrev-completion) ("C-M-/" . dabbrev-expand)) ;; Other useful Dabbrev configurations. :custom (dabbrev-ignored-buffer-regexps '("\\.\\(?:pdf\\|jpe?g\\|png\\)\\'"))) (use-package sendmail :init (setq mail-specify-envelope-from t) (setq message-sendmail-envelope-from 'header) (setq mail-envelope-from 'header) :config (if (eq system-type 'darwin) (setq sendmail-program "/usr/local/bin/msmtp") (setq sendmail-program "/usr/bin/msmtp"))) (use-package notmuch :config (defun ymhg/notmuch-search-delete-mail (&optional beg end) "Delete a message." (interactive (notmuch-interactive-region)) (if (member "deleted" (notmuch-search-get-tags)) (notmuch-search-tag (list "-deleted")) (progn (notmuch-search-tag (list "+deleted" "-unread") beg end) (notmuch-search-next-thread)))) (defun ymhg/notmuch () "Delete a message." (interactive) (let ((tab (tab-bar--tab-index-by-name "*MAIL*"))) (if tab (tab-bar-select-tab (1+ tab)) (progn (tab-bar-new-tab-to) (tab-bar-rename-tab "*MAIL*") (notmuch))))) (defun ymhg/notmuch-show-delete-mail (&optional beg end) "Delete a message." (interactive (notmuch-interactive-region)) (if (member "deleted" (notmuch-show-get-tags)) (notmuch-show-tag (list "-deleted")) (progn (notmuch-show-tag (list "+deleted" "-unread") beg end) (notmuch-show-next-thread)))) (setq notmuch-archive-tags '("-inbox" "-unread" "+archive")) (setq-default notmuch-search-oldest-first nil) (define-key notmuch-show-mode-map (kbd "d") #'ymhg/notmuch-show-delete-mail) (define-key notmuch-search-mode-map (kbd "d") #'ymhg/notmuch-search-delete-mail) (global-set-key (kbd "C-c o m") #'ymhg/notmuch) (setq notmuch-saved-searches '((:name "inbox" :query "date:last_month..this_month and tag:inbox not tag:deleted" :key "n") (:name "flagged" :query "tag:flagged" :key "f") (:name "sent" :query "tag:sent" :key "s") (:name "drafts" :query "tag:draft" :key "d") (:name "mailbox" :query "date:last_month..this_month and (tag:mailbox and tag:inbox) and not tag:deleted and not tag:sent" :key "m") (:name "imperial" :query "date:last_month..this_month and (tag:imperial and tag:inbox) and not tag:deleted and not tag:sent" :key "i") (:name "mailbox-archive" :query "date:last_month..this_month and (tag:mailbox and tag:archive) and not tag:deleted and not tag:sent" :key "a") (:name "imperial-archive" :query "date:last_month..this_month and (tag:imperial and tag:archive) and not tag:deleted and not tag:sent" :key "b") (:name "all recent" :query "date:last_month..this_month" :key "r"))) (setq notmuch-fcc-dirs '(("yann@yannherklotz.com" . "mailbox/Sent -inbox +sent -unread +mailbox -new") ("git@ymhg.org" . "mailbox/Sent -inbox +sent -unread +mailbox -new") ("yann.herklotz15@imperial.ac.uk" . "\"imperial/Sent Items\" -inbox +sent -unread +imperial -new"))) (setq +notmuch-home-function (lambda () (notmuch-search "tag:inbox")))) (use-package ol-notmuch) (use-package ebib :bind (("C-c y b" . ebib) ("C-c [" . ebib-insert-citation)) :init (defun ymhg/ebib-create-identifier (key _) key) (setq ebib-preload-bib-files '("~/Dropbox/bibliography/references.bib")) (setq ebib-notes-default-file "~/Dropbox/bibliography/notes.org") (setq ebib-notes-template "* %T\n:PROPERTIES:\n%K\n:NOTER_DOCUMENT: papers/%k.pdf\n:END:\n%%?\n") (setq ebib-keywords (expand-file-name "~/Dropbox/bibliography/keywords.txt")) (setq ebib-reading-list-file "~/Dropbox/bibliography/reading_list.org") (setq ebib-notes-storage 'multiple-notes-per-file) :config (add-to-list 'ebib-notes-template-specifiers '(?k . ymhg/ebib-create-identifier)) (add-to-list 'ebib-file-search-dirs "~/Dropbox/bibliography/papers") (if (eq system-type 'darwin) (add-to-list 'ebib-file-associations '("pdf" . "open")) (add-to-list 'ebib-file-associations '("pdf" . nil))) (add-to-list 'ebib-citation-commands '(org-mode (("ref" "[cite:@%(%K%,)]")))) (add-to-list 'ebib-citation-commands '(context-mode (("cite" "\\cite[%(%K%,)]") ("authoryear" "\\cite[authoryear][%(%K%,)]") ("authoryears" "\\cite[authoryears][%(%K%,)]") ("entry" "\\cite[entry][%(%K%,)]") ("author" "\\cite[author][%(%K%,)]")))) (advice-add 'bibtex-generate-autokey :around (lambda (orig-func &rest args) (replace-regexp-in-string ":" "" (apply orig-func args)))) (remove-hook 'ebib-notes-new-note-hook #'org-narrow-to-subtree)) (use-package ymh-ebib :straight nil :load-path "ymh-emacs" :config (define-key ebib-index-mode-map "D" #'ymh-ebib-download-pdf-from-doi)) (use-package spell-fu :hook text-mode :config (add-hook 'spell-fu-mode-hook (lambda () (spell-fu-dictionary-add (spell-fu-get-ispell-dictionary "en_GB")) (spell-fu-dictionary-add (spell-fu-get-ispell-dictionary "de_DE")) (spell-fu-dictionary-add (spell-fu-get-ispell-dictionary "fr_FR")) (spell-fu-dictionary-add (spell-fu-get-personal-dictionary "fr-personal" "~/.aspell.en_GB.pws")) (spell-fu-dictionary-add (spell-fu-get-personal-dictionary "de-personal" "~/.aspell.de_DE.pws")) (spell-fu-dictionary-add (spell-fu-get-personal-dictionary "fr-personal" "~/.aspell.fr_FR.pws"))))) (use-package ledger-mode) (use-package geiser :config ;;(unbind-key "C-." geiser-mode-map) ;;(unbind-key "C-." geiser-repl-mode-map) ) (use-package geiser-chicken :config (setq geiser-chicken-binary "chicken-csi")) (use-package bufferlo :straight (:host github :repo "florommel/bufferlo") :defer nil :bind (("C-x b" . bufferlo-switch-to-buffer)) :config (bufferlo-mode 1)) (use-package haskell-mode) (use-package proof-general :config (setq proof-splash-enable nil) (setq proof-auto-action-when-deactivating-scripting 'retract) (setq proof-delete-empty-windows nil) (setq proof-multiple-frames-enable nil) (setq proof-three-window-enable nil) (setq proof-auto-raise-buffers nil) (setq coq-compile-before-require nil) (setq coq-compile-vos t) (setq coq-compile-parallel-in-background t) (setq coq-compile-keep-going nil) (setq coq-compile-quick 'no-quick) (setq coq-max-background-compilation-jobs 4) (setq coq-indent-modulestart 0) (defun ymhg--reset-coq-indentation () "Reset slow indentation." (setq-local indent-line-function #'indent-relative)) (add-hook 'coq-mode-hook #'ymhg--reset-coq-indentation t) ;;(define-key coq-mode-map (kbd "C-c TAB") #'smie-indent-line) ) (use-package alectryon :hook (coq-mode . alectryon-mode) :delight alectryon-mode :config (when (eq system-type 'darwin) (setq alectryon-executable "/nix/store/bvlk3hyrjdgl0sg93rrdr2z71hgza0m9-python3.9-alectryon-1.4.0/bin/alectryon")) (defun ymhg/alectryon-preview () "Display an HTML preview of the current buffer." (interactive) (let* ((html-fname (make-temp-file "alectryon" nil ".html")) (args `("-r" "5" "-" ,html-fname))) (apply #'call-process-region nil nil "rst2html5" nil nil nil args) (message "Compilation complete") (browse-url html-fname))) (define-key alectryon-mode-map (kbd "C-c u t") #'alectryon-toggle) (define-key alectryon-mode-map (kbd "C-c u p") #'ymhg/alectryon-preview)) (use-package tex :straight auctex :init (setq TeX-auto-save t) (setq TeX-parse-self t) (setq-default TeX-master nil) (setq TeX-view-program-selection '((output-pdf "PDF Tools"))) (setq TeX-source-correlate-start-server t) (setq-default TeX-command-extra-options "-shell-escape") (setq TeX-source-correlate-mode t) (setq TeX-source-correlate-method 'synctex) (setq reftex-plug-into-AUCTeX t) :config (add-hook 'TeX-after-compilation-finished-functions #'TeX-revert-document-buffer) (add-hook 'TeX-mode-hook #'reftex-mode) (add-hook 'TeX-mode-hook #'outline-minor-mode) (with-eval-after-load 'latex (define-key LaTeX-mode-map " " #'ymhg/electric-space))) (use-package ox-hugo) (use-package ox-gfm) (use-package smartparens-config :straight smartparens :defer nil :config (smartparens-global-mode) (add-hook 'minibuffer-setup-hook #'turn-on-smartparens-strict-mode) (define-key smartparens-mode-map (kbd "C-M-f") #'sp-forward-sexp) (define-key smartparens-mode-map (kbd "C-M-b") #'sp-backward-sexp) (define-key smartparens-mode-map (kbd "C-M-d") #'sp-down-sexp) (define-key smartparens-mode-map (kbd "C-M-a") #'sp-backward-down-sexp) (define-key smartparens-mode-map (kbd "C-S-d") #'sp-beginning-of-sexp) (define-key smartparens-mode-map (kbd "C-S-a") #'sp-end-of-sexp) (define-key smartparens-mode-map (kbd "C-M-e") #'sp-up-sexp) (define-key smartparens-mode-map (kbd "C-M-u") #'sp-backward-up-sexp) (define-key smartparens-mode-map (kbd "C-M-t") #'sp-transpose-sexp) (define-key smartparens-mode-map (kbd "C-M-n") #'sp-forward-hybrid-sexp) (define-key smartparens-mode-map (kbd "C-M-p") #'sp-backward-hybrid-sexp) (define-key smartparens-mode-map (kbd "C-M-k") #'sp-kill-sexp) (define-key smartparens-mode-map (kbd "C-M-w") #'sp-copy-sexp) (define-key smartparens-mode-map (kbd "C-") #'sp-forward-slurp-sexp) (define-key smartparens-mode-map (kbd "C-") #'sp-forward-barf-sexp) (define-key smartparens-mode-map (kbd "C-M-") #'sp-backward-slurp-sexp) (define-key smartparens-mode-map (kbd "C-M-") #'sp-backward-barf-sexp) (define-key smartparens-mode-map (kbd "M-D") #'sp-splice-sexp) (define-key smartparens-mode-map (kbd "C-]") #'sp-select-next-thing-exchange) (define-key smartparens-mode-map (kbd "C-") #'sp-select-previous-thing) (define-key smartparens-mode-map (kbd "C-M-]") #'sp-select-next-thing) (define-key smartparens-mode-map (kbd "M-F") #'sp-forward-symbol) (define-key smartparens-mode-map (kbd "M-B") #'sp-backward-symbol) (define-key smartparens-mode-map (kbd "C-\"") #'sp-change-inner) (define-key smartparens-mode-map (kbd "M-i") #'sp-change-enclosing) (bind-key "C-c f" (lambda () (interactive) (sp-beginning-of-sexp 2)) smartparens-mode-map) (bind-key "C-c b" (lambda () (interactive) (sp-beginning-of-sexp -2)) smartparens-mode-map) (bind-key ";" #'sp-comment emacs-lisp-mode-map) (bind-key [remap c-electric-backspace] #'sp-backward-delete-char smartparens-strict-mode-map) (sp-with-modes 'org-mode (sp-local-pair "=" "=" :wrap "C-="))) (setq gc-cons-threshold (* 1024 1024 10)) (setq custom-file (concat user-emacs-directory "custom.el")) (load custom-file)