;;; -*- lexical-binding: t; -*- ;; fish as default confuses some sub processes of emacs (setq shell-file-name (executable-find "bash")) (setq ;; doom-font (font-spec :family "Hasklig" :size 15) doom-unicode-font (font-spec :family "Julia Mono")) ;; (load-theme 'doom-palenight t) (load-theme 'doom-moonlight t) ;; icons in the tray (setq display-time-24hr-format 1) (display-time-mode) (display-battery-mode) ;; company-mode auto-completion, to turn off use :company-complete (require 'company) (setq company-idle-delay 0.2 company-minimum-prefix-length 3) ;; for some reason these were broken by default (setq org-roam-capture-templates '(("d" "default" plain "" :target (file+head "%<%Y%m%d%H%M%S>-${slug}.org" "#+title: ${title}") :unnarrowed t))) (after! org (setq org-todo-keywords '((sequence "TODO" "PROGRESS" "IDEA" "IDLE" "|" "DONE" "DISCARDED") (sequence "[ ](T)" "[X](D)")) org-todo-keyword-faces '(("[-]" . +org-todo-active) ("[?]" . +org-todo-onhold) ("KILL" . +org-todo-cancel)))) (after! org-special-block-extras ; center a single-line string in a block of width (defun prooftree--center-string (width str) (-let* ((padding (- width (length str))) (half (/ padding 2)) (other (- padding half))) (s-concat (s-repeat half " ") (if (eq str nil) "" str) (s-repeat other " ")))) ;; helper (defun join-stuff (w1 lines1 lines2) (if (and (eq nil (car lines1)) (eq nil (car lines2))) "" (-let ((previous (join-stuff w1 (cdr lines1) (cdr lines2)))) (s-concat previous (if (equal previous "") "" "\n") (car lines1) (s-repeat (- w1 (length (car lines1))) " ") (car lines2))))) ;; join two proof trees line-wise, with some spacing in between (defun prooftree--linewise-join (tree1 tree2) (-let* (((w1 . str1) tree1) ((w2 . str2) tree2) (lines1 (reverse (s-split "\n" str1))) (lines2 (reverse (s-split "\n" str2))) (spacing (if (< (+ w1 w2) 4) 2 4))) `(,(+ w1 spacing w2) . ,(join-stuff (+ spacing w1) lines1 lines2)))) ;; join two proof trees line-wise, without any spacing (defun prooftree--linewise-block-join (tree1 tree2) (-let* (((w1 . str1) tree1) ((w2 . str2) tree2) (lines1 (reverse (s-split "\n" str1))) (lines2 (reverse (s-split "\n" str2)))) `(,(+ w1 w2) . ,(join-stuff w1 lines1 lines2)))) ;; center a proof tree in a block of width (defun prooftree--center-tree (width tree) (-let* (((w . _) tree) (padding (/ (- width w) 2))) (prooftree--linewise-block-join `(,padding . "") tree) )) ;; prooftree--linewise-join, but for arbitrarily many proof trees in a list (defun prooftree--join-trees (trees) (if (equal (length trees) 1) (car trees) (prooftree--join-trees `(,(prooftree--linewise-join (car trees) (cadr trees)) . ,(cddr trees))))) ;; produce readable plain text representations of proof trees (defun org--list-to-plaintext-tree (lst) (cond ((symbolp lst) '(0 . "")) ((symbolp (car lst)) (org--list-to-plaintext-tree (cadr lst))) (t (-let* (((conclusionâ‚€ children) lst) ((name named?) (s-split " :: " conclusionâ‚€)) (conclusion (or named? conclusionâ‚€))) (if (not children) (-let ((rendered (if named? (format "%s(%s)\n%s" (s-repeat (length conclusion) "-") name conclusion) conclusion)) (width (if named? (+ (length conclusion) 2 (length name)) (length conclusion)))) `(,width . ,rendered)) (-let* ((premises (cdr (mapcar #'org--list-to-plaintext-tree children))) (premises-width (+ (* 4 (- (length premises) 1)) (apply '+ (mapcar #'car premises)))) (width (+ 2 (max premises-width (length conclusion))))) `(,width . ,(format "%s\n%s%s\n%s" (cdr (prooftree--center-tree width (prooftree--join-trees premises))) (s-repeat width "-") (if named? (format "(%s)" name) "") (prooftree--center-string width conclusion))))))))) ;; same as the "tree" block, but with more than just LaTeX (org-defblock prooftree (main-arg) (let ((proof (cdr (with-temp-buffer (org-mode) ; otherwise org-list-to-lisp is unhappy (insert raw-contents) (goto-char (point-min)) (org-list-to-lisp))))) (pcase backend (`latex (s-join "" (--map (format "\\[%s\\]" (org--list-to-math it)) proof))) (_ (format "
%s
" (s-join "\n\n" (--map (format "%s" (cdr (org--list-to-plaintext-tree it))) proof))))))) ) (setq org-agenda-files '("~/org" "~/org/roam")) (setq org-roam-directory "~/org/roam") (setq org-roam-v2-ack t) ;; hooks to turn on lsp when entering haskell mode ;; TODO: not sure if necessary? (add-hook 'haskell-mode-hook #'lsp) (add-hook 'haskell-literate-mode-hook #'lsp) ;; mu4e is part of the mu system package, managed by nix (add-to-list 'load-path "~/.nix-profile/share/emacs/site-lisp/mu4e/") (after! mu4e (set-email-account! "hacc" '( (user-mail-address . "stuebinm@hacc.space") (user-full-name . "stuebinm") (m4u-maildir . "~/Maildir/hacc") (mu4e-sent-folder . "/hacc/Sent") (mu4e-trash-folder . "/hacc/Trash") ) t) (set-email-account! "disroot" '( (user-mail-address . "stuebinm@disroot.org") (user-full-name . "terru") (m4u-maildir . "~/Maildir/disroot") (mu4e-sent-folder . "/disroot/Sent") (mu4e-trash-folder . "/disroot/Trash")) t) (set-email-account! "tum" '( (user-mail-address . "stuebinm@in.tum.de") (user-full-name . "stuebinm") (m4u-maildir . "~/Maildir/tum") (mu4e-sent-folder . "/tum/Sent") (mu4e-trash-folder . "/tum/Trash")) t) (set-email-account! "ilztalbahn" '( (user-mail-address . "stuebinm@ilztalbahn.eu") (user-full-name . "terru") (m4u-maildir . "~/Maildir/ilztalbahn") (mu4e-sent-folder . "/ilztalbahn/Sent") (mu4e-trash-folder . "/ilztalbahn/Trash")) t) (setq sendmail-program (executable-find "msmtp") send-mail-function #'smtpmail-send-it message-sendmail-f-is-evil t message-sendmail-extra-arguments '("--read-envelope-from") message-send-mail-function #'message-send-mail-with-sendmail) (setq mu4e-split-view 'vertical) (setq mu4e-headers-visible-columns 80) ; initial search query ("/" by default, which makes fuzzy search annoying) (setq mu4e-maildir-initial-input "")) (after! helm-dictionary (setq helm-dictionary-database '(("de-en" . "~/org/dict/de-en.txt") ("es-de" . "~/org/dict/es-de.txt") ("en-it" . "~/org/dict/en-it-enwiktionary.txt") ("it-en" . "~/org/dict/it-en-enwiktionary.txt")))) ;; hide all these annoying popups that clutter the view (setq lsp-ui-doc-enable nil) (setq lsp-ui-sideline-show-code-actions nil) (setq lsp-signature-render-documentation nil) (after! (lsp-ui helm-lsp) (lsp-signature-activate) ;; custom version which will not blindly apply a single code action ;; if only one is available without asking about it first. ;; Source taken from https://github.com/emacs-lsp/helm-lsp/blob/master/helm-lsp.el (lsp-make-interactive-code-action wingman-fill-hole "refactor.wingman.fillHole") (lsp-make-interactive-code-action wingman-case-split "refactor.wingman.caseSplit") (lsp-make-interactive-code-action wingman-refine "refactor.wingman.refine") (lsp-make-interactive-code-action wingman-split-func-args "refactor.wingman.spltFuncArgs") (lsp-make-interactive-code-action wingman-use-constructor "refactor.wingman.useConstructor") (map! :map haskell-mode-map "C-c s" #'lsp-wingman-split "C-c h" #'lsp-wingman-fillhole) (defun helm-lsp-code-actions-custom() "Show lsp code actions using helm." (interactive) (let ((actions (lsp-code-actions-at-point))) (cond ((seq-empty-p actions) (signal 'lsp-no-code-actions nil)) (t (helm :sources (helm-build-sync-source "Code Actions" :candidates actions :candidate-transformer (lambda (candidates) (-map (-lambda ((candidate &as &CodeAction :title)) (list title :data candidate)) candidates)) :action '(("Execute code action" . (lambda(candidate) (print "selected code action") (print (plist-get candidate :data)) (lsp-execute-code-action (plist-get candidate :data))))))))))) (map! :map doom-leader-code-map "a" #'helm-lsp-code-actions-custom))