‎

(load-file "~/.config/sensitive.el")

Package Configuration

Add MELPA to the list of recognized archives

(add-to-list 'package-archives
             '("melpa" . "https://melpa.org/packages/") t)

Installs use-package if I don't have it already and enables verbose messages

(unless (package-installed-p 'use-package)
(package-install 'use-package))

(require 'use-package)
(setq use-package-verbose t)

Updates the local cache if it is missing

(unless package-archive-contents
  (package-refresh-contents))

Use-package always installs packages

(setq use-package-always-ensure t)

Install quelpa

(use-package quelpa)

GNU keys to enable downloading packages

(use-package gnu-elpa-keyring-update)

Some Miscellaneous Configurations

enable creation of pairs of brackets or quotes when one is inserted.

(setq skeleton-pair t)
(bind-key "(" 'skeleton-pair-insert-maybe)
(bind-key "{" 'skeleton-pair-insert-maybe)
(bind-key "[" 'skeleton-pair-insert-maybe)
(bind-key (char-to-string 34) 'skeleton-pair-insert-maybe)
;char 34 is the single quote, putting the character itself
;ruins prettify symbols mode

Enable Emacs to track changes made to files by different programs.

(global-auto-revert-mode 1)

Allows me to see the column number as well as the line number.

(column-number-mode)

Bookmarks are preserved throughout different sessions

(setq bookmark-save-flag 0)

Keybindings for navigating functions

(bind-key "C-M-p" #'beginning-of-defun)
(bind-key "C-M-n" #'end-of-defun)

Better scroll

(when (display-graphic-p)
  (setq mouse-wheel-scroll-amount '(2 ((shift) . 1))
        mouse-wheel-progressive-speed nil))

opens files at the last visited location

(save-place-mode 1)

don't use ui dialogs

(setq use-dialog-box nil)

Keybinding for quickly evaluating elisp code

(add-hook 'lisp-interaction-mode-hook
          (lambda () (local-set-key
                      (kbd "C-c C-c") #'eval-region)))

Suppress annoying message any time you start a new frame

(setq server-client-instructions nil)

Enable recentf mode to remember recently opened files

(recentf-mode 1)
(setq recentf-max-saved-items 10000)
(add-to-list 'recentf-exclude
           (lambda (s) (cl-search "/test/" s)))
(add-to-list 'recentf-exclude
           (lambda (s) (cl-search "/tmp/" s)))

Keybindings for splitting a window instead clones the frame

;; (bind-key "C-x 3" #'clone-frame)
;; (bind-key "C-x 2" #'clone-frame)

Every time a file is visited, update the list of recently visited files.

(add-hook 'find-file-hook 'recentf-save-list)

Add binding to go to previous and next buffer.

(winner-mode)
(global-set-key "\C-xp" 'winner-undo)
(global-set-key "\C-xn" 'winner-redo)

Set scratch buffer major mode to org-mode

(setq initial-major-mode 'org-mode)
(setq initial-scratch-message "")

Delete trailing white spaces after saving a file.

(add-hook 'before-save-hook
          'delete-trailing-whitespace)

Multiple cursors

(use-package multiple-cursors)
(global-set-key (kbd "C->") 'mc/mark-next-like-this)
(global-set-key (kbd "C-<") 'mc/mark-previous-like-this)
(global-set-key (kbd "C-c C-<") 'mc/mark-all-like-this)
(global-set-key (kbd "C-x x SPC") 'set-rectangular-region-anchor)

Yanking a string replaces the current selection

(delete-selection-mode 1)

Gospel thing

  (defun gospel-header ()
    (interactive)
    (insert "(**************************************************************************)
(*                                                                        *)
(*  GOSPEL -- A Specification Language for OCaml                          *)
(*                                                                        *)
(*  Copyright (c) 2018- The VOCaL Project                                 *)
(*                                                                        *)
(*  This software is free software, distributed under the MIT license     *)
(*  (as described in file LICENSE enclosed).                              *)
(**************************************************************************)
"))

Key binding for returning to the beginning of the line ignores indentation

(global-set-key (kbd "C-a") #'back-to-indentation)

`utf-8`

(prefer-coding-system       'utf-8)
(set-default-coding-systems 'utf-8)
(set-terminal-coding-system 'utf-8)
(set-keyboard-coding-system 'utf-8)
(setq default-buffer-file-coding-system 'utf-8)
(set-language-environment 'utf-8)
(set-selection-coding-system 'utf-8)
(setq x-select-request-type '(UTF8_STRING COMPOUND_TEXT TEXT STRING))

Backup files

Ensures that backups and auto-saves go to a separate directory instead of stinking up the working directory.

(defvar backup-dir (expand-file-name "~/.emacs.d/backup/"))
(defvar autosave-dir (expand-file-name "~/.emacs.d/autosave/"))
(setq backup-directory-alist (list (cons ".*" backup-dir)))
(setq auto-save-list-file-prefix autosave-dir)
(setq auto-save-file-name-transforms `((".*" ,autosave-dir t)))

Adds themes folder to custom themes

(add-to-list 'custom-theme-load-path "~/.config/themes/")
(add-to-list 'custom-theme-load-path
           "~/.config/themes/plasma-theme/")

Miscellaneous Packages

(use-package pacmacs)
(use-package fireplace)
(use-package mingus)
(use-package bluetooth)
(use-package trashed)
(use-package browse-kill-ring)
(global-set-key "\C-cy" #'browse-kill-ring)

(use-package avy
  :custom (avy-timeout-seconds 0.3))
(bind-key "M-j" 'avy-goto-char-timer)

(use-package exec-path-from-shell)
(when (daemonp)
  (exec-path-from-shell-initialize))

Repeat mode

This allows me to easily switch to another buffer using "p" and "n" when I have already used a buffer navigation command.

(repeat-mode 1)

(setq winner-repeat-map
      (let ((map (make-sparse-keymap)))
      (define-key map (kbd "p") 'winner-undo)
        (define-key map (kbd "n") 'winner-redo)
      map))

Disable repeat mode in Dired

(setq dired-jump-map nil)

Popup windows

I use the shackle package to control the behaviour of pop up windows.

(use-package shackle)
(setq shackle-select-reused-windows t)
(setq shackle-rules
      '(("*compilation*" :same t)
      ('magit-status-mode :same t)))
(setq shackle-inhibit-window-quit-on-same-windows t)
(shackle-mode 1)

GPG

;; let's get encryption established
(use-package pinentry)
(setenv "GPG_AGENT_INFO" nil)  ;; use emacs pinentry
(setq auth-source-debug t)

(setq epg-gpg-program "gpg2")  ;; not necessary
(require 'epa-file)
(epa-file-enable)
(setq epa-pinentry-mode 'loopback)
(setq epg-pinentry-mode 'loopback)
(pinentry-start)

(require 'org-crypt)
(org-crypt-use-before-save-magic)

(setq epa-file-encrypt-to email1)
(setq epa-file-select-keys 1)

Coding Packages

`Flymake`

Package used by Eglot for highlighting errors

(use-package flymake
  :bind (:map flymake-mode-map
         ("\C-c \C-x" . flymake-goto-next-error))
  :hook (prog-mode . flymake-mode)
  )

Company

Package for completion suggestions

(use-package company)
(global-company-mode 1)
;; (use-package corfu
;;   :custom (corfu-auto t))

;; (global-corfu-mode 1)

;; (use-package nerd-icons-corfu)
;; (add-to-list 'corfu-margin-formatters #'nerd-icons-corfu-formatter)

OCaml packages

(defun ocaml-compile ()
  (setq compile-command "~/.config/ocompile.sh")
  )

(use-package tuareg
  ;; changes the default compile command
  :hook (tuareg-mode . ocaml-compile)
  :hook (tuareg-mode . flycheck-mode))

(use-package ocamlformat
  :custom (ocamlformat-enable 'enable-outside-detected-project)
  :custom (ocamlformat-show-errors nil)
  :hook (before-save . ocamlformat-before-save))

(load "/home/tiago/.opam/4.14.1/share/emacs/site-lisp/tuareg.el")
(use-package dune)

Rust packages

(use-package rustic
  :config (setq rustic-lsp-client #'eglot))

`Eglot`

Package for language servers

(defun lsp-no-coq ()
  (interactive)
  (unless (eq major-mode 'coq-mode) (eglot-ensure)))

(use-package eglot
    :hook (prog-mode . lsp-no-coq))

Neat eldoc popup

(use-package eldoc-box
  :custom (eldoc-box-only-multi-line t))

(bind-key "\C-hj" #'eldoc-box-help-at-point)

Git packages

I will always use magit though. magit :)

(use-package magit
  :bind (:map magit-mode-map
              ("C-c C-p" . magit-section-up)))

(setq magit-display-buffer-function
      #'magit-display-buffer-traditional)

(setq magit-bury-buffer-function
      'magit-restore-window-configuration)

(bind-key "C-x g" #'magit-status)

Miscellaneous Coding Packages

(use-package yaml-mode)

`Dired`

Deleted files are moved to the trash folder

(setq delete-by-moving-to-trash t)

Start Dired in omit mode

(add-hook 'dired-mode-hook #'dired-omit-mode)

Bind the "o" key to show hidden files

(add-hook 'dired-mode-hook
          (lambda () (local-set-key
                      (kbd "o") #'dired-omit-mode)))

Bind the "b" key to move up in the directory

(add-hook 'dired-mode-hook
          (lambda () (local-set-key
                      (kbd "b") #'dired-up-directory)))

Set files to omit

(setq dired-omit-files
      (rx (or (seq bol (? ".") "#")     ;; emacs autosave files
              (seq bol ".") ;; dot-files
              (seq "~" eol)                 ;; backup-files
              (seq bol "CVS" eol)           ;; CVS dirs
            (seq bol "CVS" eol)           ;; CVS dirs
              ))
      )
(setq dired-omit-files
      (concat dired-omit-files "\\|\\.gpg$")) ;; encrypted files

Make it so Dired buffers are just a list of file names.

(add-hook 'dired-mode-hook
          (lambda () (dired-hide-details-mode 1)))

Icons for Dired mode.

 ;This package requires additional fonts
(use-package all-the-icons-dired
  :hook (dired-mode . all-the-icons-dired-mode))

Kill Dired buffer when opening a new Dired buffer.

(setq dired-kill-when-opening-new-dired-buffer t)

Dired buffers update when there is a change in one of the files in the directory

(setq global-auto-revert-non-file-buffers t)

Keeps track of visited Dired buffers

(use-package dired-hist)
(define-key dired-mode-map "l" #'dired-hist-go-back)
(define-key dired-mode-map "r" #'dired-hist-go-forward)
(dired-hist-mode 1)

More convenient way to search through sub-directories.

(use-package dired-subtree
  :bind (:map dired-mode-map
        ("i" . dired-subtree-insert)
        ("DEL" . dired-subtree-remove)))

Disable "Omit N files" message

(setq dired-omit-verbose nil)

Quickly browse files in read only mode

(defun view-browse (f)

  (let ((b (current-buffer)))
    (dired-jump)
    (condition-case nil
      ((lambda () (funcall f)
         (dired-find-file)
         (kill-buffer b)
         (view-mode)))
      (error
       (progn (switch-to-buffer b)
            (message "No more files in current directory"))))))

(defun view-next-file ()
  (interactive)
  (view-browse (lambda () (dired-next-line 1))))

(defun view-previous-file ()
  (interactive)
  (view-browse (lambda () (dired-previous-line 1)))
  )

(define-key view-mode-map (kbd "n") 'view-next-file)
(define-key view-mode-map (kbd "p") 'view-previous-file)

Change ls switches to use human readable file sizes

(setq dired-listing-switches "-alh")

When copying a file, have it so if there is another dired buffer open in another window in the same frame, it selects that buffer by default

(setq dired-dwim-target t)

Org

Some Basic Bookkeeping

Some helpful variables

(defun org-directory (file)
  (concat "~/roam/daily/personal/" file))

(defvar todo-file
  (org-directory "todo.org.gpg"))

(defvar agenda-file
  (org-directory "appoint.org.gpg"))

My agenda files:

(setq org-agenda-file-regexp "\\`[^.].*\\.org\\\(\\.gpg\\\)?\\'")
(setq org-agenda-files (list (org-directory "")))

Settings for exporting Org files with citations to TeX.

  (setq org-cite-export-processors '((t biblatex "numeric" "numeric")))
;  (setq org-cite-global-bibliography '("~/org/org.bib"))
  (setq org-export-with-sub-superscripts nil)

Enable notifications for Org agenda items

(use-package org-alert
  :custom (alert-default-style 'libnotify)
  :custom (org-alert-interval 300)
  :custom (org-alert-notify-cutoff 10)
  :custom (org-alert-notify-after-event-cutoff 0)
  )
(org-alert-enable)

Add menu item to list only items with a TODO keyword.

(setq org-agenda-custom-commands
      '(("t" "List all items with the TODO keyword" ((todo "TODO")))))

This is very important

(defun what ()
  (interactive)
  (insert "👁️👄👁️")
  )

Appearance

Hide emphasis markers and macro braces

(setq org-hide-emphasis-markers t)
(setq org-hide-macro-markers t)

Make it there is only one star visible in each heading.

(setq org-hide-leading-stars t)

Use LaTeX like syntax to insert special symbols

(setq org-pretty-entities t)

Start Org files with each heading folded.

(setq org-startup-folded t)

Enable Org indentation

(setq org-startup-indented t)
(use-package org-modern-indent
  :load-path "~/"
  ; or
  ; :straight (org-modern-indent :type git :host github :repo "jdtsmith/org-modern-indent"))
  :config ; add late to hook
  (add-hook 'org-mode-hook #'org-modern-indent-mode 90))

Centre Org agenda

(add-hook 'org-agenda-mode-hook #'writeroom-mode)

Don't show items that are marked as done.

(setq org-agenda-skip-timestamp-if-done t
      org-agenda-skip-deadline-if-done t
      org-agenda-skip-scheduled-if-done t
      org-agenda-skip-scheduled-if-deadline-is-shown t
      org-agenda-skip-timestamp-if-deadline-is-shown t)

Automatic latex preview in Org mode

(setq org-startup-with-latex-preview t)

(use-package org-fragtog
  :hook (org-mode . org-fragtog-mode))

Scale up latex preview in Org mode

(setq org-format-latex-options
      (plist-put org-format-latex-options :scale 3))

Automatically converts strings to emojis

(use-package emojify)

Org Pretty Symbols

Function for adding pretty symbols for Org mode. Most of these are just so that Org mode environments aren't awful to look at.

  ;; Pretty Symbols for Org
(defun add-symbols ()
  (push '("#+end_example" . ? ) prettify-symbols-alist)
  (push '("#+end_src" . ? ) prettify-symbols-alist)
  (push '("#+begin_example coq" . ?🐓) prettify-symbols-alist)
  (push '("#+begin_example ocaml" . ?🐫) prettify-symbols-alist)
  (push '("#+begin_src ocaml" . ?🐫) prettify-symbols-alist)
  (push '("#+begin_example ocaml :why3" . ?❔) prettify-symbols-alist)
  ;;errrrrrm, what the ...
  (push '("#+begin_src emacs-lisp :results none" . ?🗿) prettify-symbols-alist)
  (push '("#+ATTR_LATEX: :environment cfml" . ? ) prettify-symbols-alist)
  (push '("#+ATTR_LATEX: :environment ocamlenv" . ? ) prettify-symbols-alist)
  (push '("#+ATTR_LATEX: :environment gospel" . ? ) prettify-symbols-alist)
  (push '("#+ATTR_LATEX: :environment whylang" . ? ) prettify-symbols-alist)
  (push '("->" . ?→) prettify-symbols-alist)
  (push '("<->" . ?↔) prettify-symbols-alist)
  (push '("|-" . ?⊢) prettify-symbols-alist)
  (push '("/\\" . ?∧) prettify-symbols-alist)
  (push '("\\/" . ?∨) prettify-symbols-alist)
  (push '("<-" . ?←) prettify-symbols-alist)
  (prettify-symbols-mode 1))

Org capture templates

(setq org-capture-templates
      '(
        ("w" "Writing TODO"
         entry (file+headline todo-file "Writing")
         "* TODO %?\n "
         :empty-lines 0)

        ("p" "Phd TODO"
         entry (file+headline todo-file "PhD Tasks")
         "* TODO [[%L][%?]]\n "
         :empty-lines 0)

        ("a" "Appointment"
         entry (file+headline agenda-file "Appointments")
         "* APPOINTMENT %?\n "
         :empty-lines 0)

        ("?" "Question"
         entry (file+headline todo-file "Questions")
         "* 👁️👄👁️ %?\n "
         :empty-lines 0)

        ("r" "Reading"
         checkitem (file+headline todo-file "Reading List")
         "[ ] %?\n")
      ))

Org Keywords

(setq org-todo-keywords
      '((sequence "APPOINTMENT(p)" "TODO(t)" "IN-PROGRESS(i@/!)" "VERIFYING(v!)" "BLOCKED(b@)" "👁️👄👁️(q)" "|" "DONE(d!)" "OBE(o@!)" "WONT-DO(w@/!)" )
        ))
;; TODO colors
(setq org-todo-keyword-faces
      '(
        ("TODO" . (:foreground "GoldenRod" :weight bold))
        ("APPOINTMENT" . (:foreground "DeepPink" :weight bold))
        ("IN-PROGRESS" . (:foreground "Cyan" :weight bold))
        ("VERIFYING" . (:foreground "DarkOrange" :weight bold))
        ("BLOCKED" . (:foreground "Red" :weight bold))
        ("DONE" . (:foreground "LimeGreen" :weight bold))
        ("WONT-DO" . (:foreground "LimeGreen" :weight bold))
        ))

Inserting Org Example Blocks

Function for wrapping text around a block

(defun tag-word-or-region (text-begin text-end)
"Surround current word or region with given text."
(interactive "sStart tag: \nsEnd tag: ")
(let (pos1 pos2 bds)
  (if (and transient-mark-mode mark-active)
      (progn
        (goto-char (region-end))
        (insert text-end)
        (goto-char (region-beginning))
        (insert text-begin))
    (progn
      (setq bds (point))
      (goto-char bds)
      (insert text-end)
      (goto-char bds)
      (insert text-begin)))))

Associative list that maps environment names to programming languages

(setq env-map '( ("cfml" . "coq")
  ("ocamlenv" . "ocaml")
  ("gospel" . "ocaml")
  ("whylang" . "ocaml :why3")
))

Function to wrap text around an example block

(defun org-insert-code-env (env-name)
  (interactive "sEnvironment name: ")
  (if (equal env-name "elisp")
      (tag-word-or-region
       "#+begin_src emacs-lisp :results none\n"
       "\n#+end_src"
       )
    (tag-word-or-region
     (concat "#+ATTR_LATEX: :environment " env-name
                              "\n#+begin_example " (alist-get env-name env-map nil nil #'equal) "\n")
                      "\n#+end_example"
                      )))

Function to insert a macro

(defun org-insert-macro ()
  (interactive)
  (tag-word-or-region "{{{" "}}}") )

Remove Spell Checking in Code Blocks

(add-to-list 'ispell-skip-region-alist '("^#\\+BEGIN_SRC" . "#\\+END_SRC"))
(add-to-list 'ispell-skip-region-alist '("^#\\+BEGIN_EXAMPLE" . "#\\+END_EXAMPLE"))
(add-to-list 'ispell-skip-region-alist '("^#\\+begin_src" . "#\\+end_src"))
(add-to-list 'ispell-skip-region-alist '("^#\\+begin_example" . "#\\+end_example"))
(add-to-list 'ispell-skip-region-alist '("^#\\+" . "\n"))
(add-to-list 'ispell-skip-region-alist '("~" . "~"))
(add-to-list 'ispell-skip-region-alist '("/" . "/"))
(add-to-list 'ispell-skip-region-alist '("{{{" . "}}}"))
(add-to-list 'ispell-skip-region-alist '("<<" . ">>"))

Org Key Bindings and Hooks

Global key bindings to access and update the agenda.

(global-set-key "\C-ca" 'org-agenda)
(global-set-key "\C-cc" 'org-capture)

Concise way of using the previous definitions to configure Org.

(use-package org
  :hook (org-mode . add-symbols)
  :bind
  (:map org-mode-map
        ("C-c C-x C-x" . org-insert-code-env))
  :bind
  (:map org-mode-map
        ("C-c C-x C-m" . org-insert-macro))
  )

French Notes

Function for inserting a conjugation table for french verbs

(setq conjugation-table
"|-----------+---|
| Je        |   |
|-----------+---|
| Tu        |   |
|-----------+---|
| Il/Elle   |   |
|-----------+---|
| Nous      |   |
|-----------+---|
| Vous      |   |
|-----------+---|
| Ils/Elles |   |
|-----------+---|")

(defun start-conjugation ()
  (interactive)
  (insert conjugation-table)
  (org-backward-paragraph)
  (org-cycle)
  (org-cycle))

LaTeX export

Add common scientific paper classes.

(with-eval-after-load 'ox-latex
  (add-to-list 'org-latex-classes
               '("llncs"
                 "\\documentclass{llncs}"
                 ("\\section{%s}" . "\\section*{%s}")
                 ("\\subsection{%s}" . "\\subsection*{%s}"))))

(with-eval-after-load 'ox-latex
  (add-to-list 'org-latex-classes
               '("IEEEtran"
                 "\\documentclass{IEEEtran}"
                 ("\\section{%s}" . "\\section*{%s}")
                 ("\\subsection{%s}" . "\\subsection*{%s}"))))

Function to create a latex project.

(defun latex-project (title class)
  (interactive "sTitle: \nsClass: ")
  (mkdir title)
  (cd title)
  (let ((d default-directory))
    (find-file "~/org/latex-templates/latex.org")
    (beginning-of-buffer)
    (let ((b (current-buffer)))
      (replace-string "?title" title)
      (replace-string "?class" class)
      (if (string= class "beamer")
          (org-beamer-export-as-latex)
        (org-latex-export-as-latex)
        )
      (let ((f (current-buffer)))
        (copy-file "config.tex" d)
        (copy-file "Makefile" d)
        (copy-file "mymacros.tex" d)
        (copy-file "gospel.sty" d)
        (copy-file "why3lang.sty" d)
        (copy-file "lstcoq.sty" d)
        (copy-file ".gitignore" d)
        (copy-file "bibliography.bib" d)
        (when (or (string= class "llncs") (string= class "IEEEtran"))
          (copy-file (concat class ".cls") d))
        (write-file (concat d "/main.tex"))
        (switch-to-buffer b)
        (set-buffer-modified-p nil)
        (kill-buffer b)
        (switch-to-buffer f)
        ))))

Org Roam

(use-package org-roam
  :custom
  (org-roam-directory (file-truename "~/roam"))
  (org-roam-file-exclude-regexp '("data/" "daily/"))
  (org-roam-completion-everywhere t)
  :bind (("C-c n l" . org-roam-buffer-toggle)
         ("C-c n f" . org-roam-node-find)
         ("C-c n g" . org-roam-graph)
         ("C-c n i" . org-roam-node-insert)
         ("C-c n c" . org-roam-capture)
         ;; Dailies
         ("C-c n j" . org-roam-dailies-capture-today)))

(org-roam-db-autosync-mode)

Capture templates for org roam.

(setq org-roam-capture-templates
      '(("t" "travel" plain
         "%?"
         :if-new (file+head "travel/%<%Y%m%d%H%M%S>-${slug}.org" "#+title: ${title}\n")
         :unnarrowed t)
      ("r" "Reading note" plain
       (file "~/roam/templates/reading_template.org")
       :if-new (file+head "research/%<%Y%m%d%H%M%S>-${slug}.org" "#+title: ${title}\n")
       :unnarrowed t)
      ("p" "PhD Note" plain
         "%?"
         :if-new (file+head "research/%<%Y%m%d%H%M%S>-${slug}.org" "#+title: ${title}\n")
         :unnarrowed t)
      ))

Capture template for org roam dailies

(setq org-roam-dailies-capture-templates
      '(("d" "default" entry "* %?" :target (file+head "%<%Y-%m-%d>.org.gpg" "#+title: %<%Y-%m-%d>
"))))

PDFs

Opens the current file in zathura and kills the Doc View buffer.

(defun zathura ()
  (when (equal (file-name-extension (buffer-file-name)) "pdf")
  (start-process "zathura" nil "zathura" (buffer-file-name))
  (let ((b (current-buffer)))
    (add-to-list 'recentf-list (buffer-file-name))
    (recentf-save-list)
    (previous-buffer)
    (kill-buffer b)
  )))

When we open a PDF in Emacs, open it in zathura instead.

(add-hook 'doc-view-mode-hook #'zathura)

Proof General

Function for a more convenient Coq buffer split.

(defun split-proof-general ()
  (interactive)
  (let ((f1 (selected-frame)) (f2 (clone-frame)))
    (select-frame f1)
    (delete-other-windows)
    (select-frame f2)
    (delete-window)
    (select-frame-set-input-focus f1) ; doesn't work! argh!
    )
  )

Package for working with Coq

(use-package proof-general
  :bind (:map coq-mode-map
              ("C-c C-k" . split-proof-general))
  :custom
  ;; when starting a proof, splits windows so that the goals
  ;; window is larger than the response window
  (proof-three-window-mode-policy 'hybrid)
  ;; Removes the EXTREMELY annoying proof general splash screen
  (proof-splash-enable nil))

Weird arrow :/

(setq overlay-arrow-string "")

Unicode Symbols for Iris

;; Input of unicode symbols
(require 'math-symbol-lists)
                                      ; Automatically use math input method for Coq files
(add-hook 'coq-mode-hook (lambda () (set-input-method "math")))
                                      ; Input method for the minibuffer
(defun my-inherit-input-method ()
  "Inherit input method from `minibuffer-selected-window'."
  (let* ((win (minibuffer-selected-window))
         (buf (and win (window-buffer win))))
    (when buf
      (activate-input-method (buffer-local-value 'current-input-method buf)))))
(add-hook 'minibuffer-setup-hook #'my-inherit-input-method)
                                      ; Define the actual input method
(quail-define-package "math" "UTF-8" "Ω" t)
(quail-define-rules ; add whatever extra rules you want to define here...
 ("\\fun"    ?λ)
 ("\\mult"   ?⋅)
 ("\\ent"    ?⊢)
 ("\\valid"  ?✓)
 ("\\diamond" ?◇)
 ("\\box"    ?□)
 ("\\bbox"   ?■)
 ("\\later"  ?▷)
 ("\\pred"   ?φ)
 ("\\and"    ?∧)
 ("\\or"     ?∨)
 ("\\comp"   ?∘)
 ("\\ccomp"  ?◎)
 ("\\all"    ?∀)
 ("\\ex"     ?∃)
 ("\\to"     ?→)
 ("\\sep"    ?∗)
 ("\\lc"     ?⌜)
 ("\\rc"     ?⌝)
 ("\\Lc"     ?⎡)
 ("\\Rc"     ?⎤)
 ("\\lam"    ?λ)
 ("\\empty"  ?∅)
 ("\\Lam"    ?Λ)
 ("\\Sig"    ?Σ)
 ("\\-"      ?∖)
 ("\\aa"     ?●)
 ("\\af"     ?◯)
 ("\\auth"   ?●)
 ("\\frag"   ?◯)
 ("\\iff"    ?↔)
 ("\\gname"  ?γ)
 ("\\incl"   ?≼)
 ("\\latert" ?▶)
 ("\\update" ?⇝)
 ("\\nin" ?∉)
 ("\\u" ?∪)
 ("\\points" ?↦)

 ;; accents (for iLöb)
 ("\\\"o" ?ö)

 ;; subscripts and superscripts
 ("^^+" ?⁺) ("__+" ?₊) ("^^-" ?⁻)
 ("__0" ?₀) ("__1" ?₁) ("__2" ?₂) ("__3" ?₃) ("__4" ?₄)
 ("__5" ?₅) ("__6" ?₆) ("__7" ?₇) ("__8" ?₈) ("__9" ?₉)

 ("__a" ?ₐ) ("__e" ?ₑ) ("__h" ?ₕ) ("__i" ?ᵢ) ("__k" ?ₖ)
 ("__l" ?ₗ) ("__m" ?ₘ) ("__n" ?ₙ) ("__o" ?ₒ) ("__p" ?ₚ)
 ("__r" ?ᵣ) ("__s" ?ₛ) ("__t" ?ₜ) ("__u" ?ᵤ) ("__v" ?ᵥ) ("__x" ?ₓ)
 )
(mapc (lambda (x)
        (if (cddr x)
            (quail-defrule (cadr x) (car (cddr x)))))
                                      ; need to reverse since different emacs packages disagree on whether
                                      ; the first or last entry should take priority...
                                      ; see <https://mattermost.mpi-sws.org/iris/pl/46onxnb3tb8ndg8b6h1z1f7tny> for discussion
      (reverse (append math-symbol-list-basic math-symbol-list-extended)))

Settings for Text Mode

Enable auto-fill.

(add-hook 'text-mode-hook #'auto-fill-mode)

Enable Writeroom mode for a more comfortable writing experience.

(use-package writeroom-mode
  :hook (text-mode . writeroom-mode)
  :custom (writeroom-mode-line t)
  :custom (writeroom-maximize-window nil)
  )

Use aspell as default spell checking program (should be default, but something is changing it)

(setq ispell-program-name "/usr/bin/aspell")

Enable Flyspell for spell checking

(use-package flyspell
  :hook (text-mode . flyspell-mode)
  :hook (prog-mode . flyspell-prog-mode))

(use-package flyspell-correct
  :bind
  (:map flyspell-mode-map
        ("C-c  $" . flyspell-correct-wrapper)
        ))

(use-package flyspell-correct-ivy)

Removes completion at point from flyspell so that I can use it for completing org roam nodes.

(keymap-unset flyspell-mode-map "C-M-i")

Package for TeX files

(use-package auctex)

Disable word completion in text-mode

(setq text-mode-ispell-word-completion nil)

Ivy

Default ivy configuration

(use-package ivy)
(ivy-mode)
(setq enable-recursive-minibuffers t)
(use-package swiper)
(use-package counsel)
;; enable this if you want `swiper' to use it
(setq search-default-mode #'char-fold-to-regexp)
(global-set-key "\C-s" 'swiper)
(global-set-key (kbd "C-c C-r") 'ivy-resume)
(global-set-key (kbd "<f6>") 'ivy-resume)
(global-set-key (kbd "M-x") 'counsel-M-x)
(global-set-key (kbd "C-x C-f") 'counsel-find-file)
(global-set-key (kbd "<f1> l") 'counsel-find-library)
(global-set-key (kbd "<f2> i") 'counsel-info-lookup-symbol)
(global-set-key (kbd "<f2> u") 'counsel-unicode-char)
(global-set-key (kbd "C-c g") 'counsel-git)
(global-set-key (kbd "C-c j") 'counsel-git-grep)
(global-set-key (kbd "C-c k") 'counsel-ag)
(global-set-key (kbd "C-x l") 'counsel-locate)
(global-set-key (kbd "C-S-o") 'counsel-rhythmbox)
(global-set-key (kbd "C-x C-b") 'counsel-recentf)
(define-key minibuffer-local-map (kbd "C-r") 'counsel-minibuffer-history)

Don't show number of candidates

(setq ivy-count-format "")

Ivy ignores order in which words are written

(setq ivy-re-builders-alist
      '((t . ivy--regex-plus)))

Sort commands and buffers by most recently used

(use-package smex)

Remove stupid ^

(setq ivy-initial-inputs-alist nil)

Ivy ignores the order in which words are typed.

(setq ivy-re-builders-alist
      '((t . ivy--regex-ignore-order)))

Ivy buffer with icons and more information

(use-package all-the-icons
  :if (display-graphic-p)
  :config
  (setq all-the-icons-scale-factor 0.8))

(use-package all-the-icons-ivy-rich
  :after counsel-projectile
  :config
  (setq all-the-icons-ivy-rich-icon-size 0.8))

(use-package ivy-rich
  :after all-the-icons-ivy-rich)

(ivy-rich-mode 1)
(all-the-icons-ivy-rich-mode 1)

Allows to select the prompt instead of a listed candidate. Mostly useful when creating and renaming files

(setq ivy-use-selectable-prompt t)

Ivy completion now pops up in dedicated frame

(use-package ivy-posframe)
(ivy-posframe-mode 1)

Non-transparent posframe

(setq ivy-posframe-parameters '((alpha . 100)))

Do not use a posframe for swiper

(setq ivy-posframe-display-functions-alist
      '((swiper          . ivy-display-function-fallback)
        (t               . ivy-posframe-display)))

Fixed width for ivy posframe

(defun my-ivy-posframe-get-size ()
  "Set the ivy-posframe size according to the current frame."
  (let ((height (or ivy-posframe-height (or ivy-height 10)))
        (width (min (or ivy-posframe-width 200) (round (* .9 (frame-width))))))
    (list :height height :width width :min-height height :min-width width)))

(setq ivy-posframe-size-function 'my-ivy-posframe-get-size)

Absolutely no idea what this does, but it makes ivy rich mode not slow as a brick

(eval-after-load 'ivy-rich
  (progn
    (defvar ek/ivy-rich-cache
      (make-hash-table :test 'equal))

    (defun ek/ivy-rich-cache-lookup (delegate candidate)
      (let ((result (gethash candidate ek/ivy-rich-cache)))
        (unless result
          (setq result (funcall delegate candidate))
          (puthash candidate result ek/ivy-rich-cache))
        result))

    (defun ek/ivy-rich-cache-reset ()
      (clrhash ek/ivy-rich-cache))

    (defun ek/ivy-rich-cache-rebuild ()
      (mapc (lambda (buffer)
              (ivy-rich--ivy-switch-buffer-transformer (buffer-name buffer)))
            (buffer-list)))

    (defun ek/ivy-rich-cache-rebuild-trigger ()
      (ek/ivy-rich-cache-reset)
      (run-with-idle-timer 1 nil 'ek/ivy-rich-cache-rebuild))

    (advice-add 'ivy-rich--ivy-switch-buffer-transformer :around 'ek/ivy-rich-cache-lookup)
    (advice-add 'ivy-switch-buffer :after 'ek/ivy-rich-cache-rebuild-trigger)))

Appearance

Disable Splash Screen

(setq inhibit-splash-screen nil)

Define font style and height

(setq default-frame-alist '((font . "Roboto Mono 22")))
(add-to-list 'default-frame-alist '(background-color . "#34293E"))

Set theme (currently Shades of Purple)

(setq custom-safe-themes t)
(setq custom-enabled-themes '(shades-of-purple))
 (load-theme 'shades-of-purple)
 ;; (use-package ef-themes
 ;;   :config (ef-themes-select 'ef-summer))
;(load-theme 'plasma-dark)

Disables a bunch of needless UI noise.

(cond ((> emacs-major-version 20)
       (tool-bar-mode -1) ; introduced in emacs 21
       (menu-bar-mode -1)
       (scroll-bar-mode -1)
       (menu-bar-showhide-fringe-menu-customize-disable)
       (blink-cursor-mode -1)
       (windmove-default-keybindings 'meta)))

Pretty mode line

(use-package doom-modeline)
(doom-modeline-mode 1)

(use-package doom-modeline-now-playing)
(doom-modeline-now-playing-timer)

(doom-modeline-def-modeline 'main
  '(bar matches buffer-info buffer-position now-playing)
  '(time major-mode))

Transparent emacs frames.

(set-frame-parameter (selected-frame) 'alpha '(80 . 80))
(add-to-list 'default-frame-alist '(alpha . (70 . 70)))

Display time in mode line

(display-time-mode 1)

Email

(setq message-send-mail-function 'smtpmail-send-it)

(require 'mu4e)

(setq user-mail-address "tl.soares@campus.fct.unl.pt")
(use-package mu4e
  :ensure nil
  ;; :load-path "/usr/share/emacs/site-lisp/mu4e/"
  ;; :defer 20 ; Wait until 20 seconds after startup
  :bind (:map mu4e-headers-mode-map
            ("q" . mu4e-dashboard))
  :config

  ;; This is set to 't' to avoid mail syncing issues when using mbsync
  (setq mu4e-change-filenames-when-moving t)
  (setq mu4e-context-policy "pick-first")
  ;; Refresh mail using isync every minute
  (setq mu4e-update-interval 60)
  (setq mu4e-get-mail-command "mbsync -a")

  (setq mu4e-maildir "~/mail")

  (setq mu4e-contexts
        (list
         ;; Work account
         (make-mu4e-context
          :name "FCT"
          :match-func
          (lambda (msg)
            (when msg
              (string-prefix-p "/gmail" (mu4e-message-field msg :maildir))))
          :vars `((user-mail-address . ,email1)
                  (user-full-name    . "Tiago Soares")
                (smtpmail-smtp-server . "smtp.gmail.com")
                (smtpmail-smtp-service . 465)
                (smtpmail-stream-type . ssl)
                  (mu4e-drafts-folder  . "/gmail/[Gmail]/Drafts")
                  (mu4e-sent-folder  . "/gmail/[Gmail]/Sent Mail")
                  (mu4e-refile-folder  . "/gmail/[Gmail]/All Mail")
                  (mu4e-trash-folder  . "/gmail/[Gmail]/Trash")))
       (make-mu4e-context
          :name "Inria"
          :match-func
          (lambda (msg)
            (when msg
              (string-prefix-p "/inria" (mu4e-message-field msg :maildir))))
          :vars `((user-mail-address . ,email2)
                  (user-full-name    . "Tiago Soares")
                (smtpmail-smtp-server . "smtp.inria.fr")
                (smtpmail-smtp-service . 587)
                (smtpmail-stream-type . nil)
                  (mu4e-drafts-folder  . "/inria/Drafts")
                  (mu4e-sent-folder  . "/inria/Sent")
                  (mu4e-trash-folder  . "/inria/Trash")))

       )
      )
  (setq mu4e-maildir-shortcuts
      '(("/gmail/inbox"             . ?f)
          ("/inria/inbox"             . ?i)
          ("/gmail/[Gmail]/Trash"     . ?t)
          ("/gmail/[Gmail]/Drafts"    . ?d)
          ("/gmail/[Gmail]/All Mail"  . ?a)))
  )

(use-package mu4e-alert)
(mu4e-alert-enable-notifications)

(use-package go-translate)
(setq gt-langs '(fr en))
(setq gt-default-translator (gt-translator :engines (gt-google-engine)))

;; This configuration means:
;; Initialize the default translator, let it translate between en and fr via Google Translate,
;; and the result will be displayed in the Echo Area.

(setq gt-default-translator
      (gt-translator
       :taker   (gt-taker :text 'buffer :pick 'paragraph)  ; config the Taker
       :engines (list (gt-bing-engine) (gt-google-engine)) ; specify the Engines
       :render  (gt-buffer-render)))                       ; config the Render

(setq mu4e-headers-fields '((:human-date . 12) (:from . 22) (:subject)))

;; This configuration means:
;; Initialize the default translator, let it send all paragraphs in the buffer to Bing and Google,
;; and output the results with a new Buffer.

;; This configuration means:
;; Initialize the default translator, let it translate between en and fr via Google Translate,
;; and the result will be displayed in the Echo Area.

(add-hook 'mu4e-view-mode-hook #'writeroom-mode)
(add-hook 'mu4e-headers-mode-hook #'writeroom-mode)
(add-hook 'message-mode-hook #'auto-fill-mode)
(load "~/.mu4e-dashboard/mu4e-dashboard.el")

(mu4e)

(setq message-cite-reply-position 'above)

(setq mu4e-hide-index-messages t)

`Eshell`

Fish like suggestions for eshell

(use-package company)

(use-package esh-autosuggest
  :hook (eshell-mode . esh-autosuggest-mode)
  :custom (eshell-history-size 50000)
  ; since esh autosuggest uses the eshell history, we increase it so
  ; that we have more possible suggesions
  :custom (company-minimum-prefix-length 1)
  :bind (:map esh-autosuggest-active-map
              ("C-f" . esh-autosuggest-complete-word)
              ("C-e" . company-complete))
  )

Pretty eshell prompt

(load-file "/home/tiago/.config/prompt.el")
(setq eshell-prompt-function #'epe-theme-dakrone)

Function for clearing the shell

(defun eshell-clear ()
  (interactive)
  "Clear the eshell buffer."
  (let ((inhibit-read-only t))
    (erase-buffer)
    (eshell-send-input)
    (beginning-of-buffer)
    (kill-line)
    (end-of-buffer)
    ))

Function for getting to the base of any project. Useful for spawning shells since having it at the root of the project is generally more convenient.

(defvar project-files
  '("dune-project" "package.json"
    "CoqProject" "Makefile"
    )
  )

(defun is-base ()
  (or (equal default-directory "/")
      (not (eq (seq-intersection
         (directory-files ".")
         project-files
         'equal
         ) nil)
      ))
  )

(defun get-to-base ()
  (let ((c default-directory))
  (progn
    (while (not (is-base))
      (find-file ".."))
    (when (equal default-directory "/")
        (find-file c)
        )
  )))

Always spawns eshell on a new terminal

(defun multi-eshell ()
  (interactive)
  (let ((b (current-buffer)))
  (when (seq-find
         (lambda (val)
           (equal "*eshell*" (buffer-name val)))
         (buffer-list))
    (switch-to-buffer "*eshell*")
    (rename-uniquely))
  (switch-to-buffer b)
  (eshell)))

Key binding for spawning a new instance of eshell at the root of a project.

(defun eshell-spawn ()
  (interactive)
  (get-to-base)
  (multi-eshell))
(bind-key "C-c C-SPC" 'eshell-spawn)

Delete duplicates in the eshell history

(setq eshell-hist-ignoredups t)

Function to run eshell command.

(defun eshell-send-command (s)
  (interactive)
  (eshell-return-to-prompt)
  (insert s)
  (eshell-send-input))

Augments eshell's completion framework so that it behaves more like fish (e.g. "pacman -S …" completes the name of the package)

(use-package fish-completion)
(global-fish-completion-mode 1)

I never know man

(setq eshell-cmpl-dir-ignore "\\`\\(CVS\\)/\\'")

Add rust packages to path

(add-to-list 'exec-path "~/.cargo/bin")

(defun set-envs (l) (dolist (p (nth 0 l)) (setenv (nth 0 p) (nth 1 p))))

Buffer name matches eshell directory

(defun sync-dir-in-buffer-name ()
    (rename-buffer (concat "*eshell* " default-directory)))

(add-hook 'eshell-directory-change-hook #'sync-dir-in-buffer-name)

`Eshell` configuration

Startup configuration. Sets the opam environment variables and runs fastfetch.

(add-hook 'eshell-mode-hook
        (lambda ()
          (define-key eshell-mode-map (kbd "C-l") #'eshell-clear)))

(defun startup ()
  (interactive)
  (eshell-send-command "opam-set && fastfetch")
  (let ((inhibit-read-only t))
    (eshell-previous-prompt 1)
    (beginning-of-line)
    (kill-line)
    (kill-line)
    (eshell-next-prompt 1)))

(require 'eshell)
(use-package eshell
  :hook (eshell-mode . startup)
  :custom (eshell-banner-message "")
  )

Configuration for Visual Commands

We use eat to run any commands that require visuals

(use-package eat
  :custom (eat-kill-buffer-on-exit t)
  :hook (eshell-mode . eat-eshell-mode)
  )

Package Configuration

Some Miscellaneous Configurations

utf-8

Backup files

Miscellaneous Packages

Repeat mode

Popup windows

GPG

Coding Packages

Flymake

Company

OCaml packages

Rust packages

Eglot

Git packages

Miscellaneous Coding Packages

Dired

Org

Some Basic Bookkeeping

Appearance

Org Pretty Symbols

Org capture templates

Org Keywords

Inserting Org Example Blocks

Remove Spell Checking in Code Blocks

Org Key Bindings and Hooks

French Notes

LaTeX export

Org Roam

PDFs

Proof General

Unicode Symbols for Iris

Settings for Text Mode

Ivy

Appearance

Email

Eshell

Eshell configuration

Configuration for Visual Commands

`utf-8`

`Flymake`

`Eglot`

`Dired`

`Eshell`

`Eshell` configuration