From dc9990e084996c1de7ee41fa293a3f77b9737cea Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 8 Apr 2023 13:01:17 +0100
Subject: Add tweaks to isearch and dafny

---
 init.el                 | 58 +++++++++++++++++++++++++++++++++----------------
 ymh-emacs/ymh-common.el |  7 +++---
 2 files changed, 43 insertions(+), 22 deletions(-)

diff --git a/init.el b/init.el
index b1061da..763977e 100644
--- a/init.el
+++ b/init.el
@@ -84,6 +84,11 @@ Should be one of `:white-split', `:modified' or `:default'")
 (use-package emacs
   :init
   (setq native-comp-async-report-warnings-errors nil)
+
+  (setq isearch-lax-whitespace t)
+  (setq isearch-regexp-lax-whitespace t)
+  (setq search-whitespace-regexp "[ \t\r\n]+")
+
   (setq gnus-init-file (expand-file-name "gnus.el" user-emacs-directory))
 
   (setq-default fill-column 80)
@@ -91,10 +96,6 @@ Should be one of `:white-split', `:modified' or `:default'")
   (setq completion-cycle-threshold 3)
   (setq tab-always-indent 'complete)
 
-  (if ymh/macos-p
-      (setq shell-file-name "/usr/local/bin/fish")
-    (setq shell-file-name "/usr/bin/fish"))
-
   (setq use-short-answers t)
   (setq inhibit-startup-message t)
   (setq confirm-nonexistent-file-or-buffer nil)
@@ -154,6 +155,8 @@ Should be one of `:white-split', `:modified' or `:default'")
 
   (setq auth-sources '("~/.authinfo" "~/.authinfo.gpg" "~/.netrc"))
   (setq wdired-allow-to-change-permissions t)
+
+  (setq visual-line-fringe-indicators '(left-curly-arrow nil))
   :config
   (unless ymh/macos-p
     (menu-bar-mode -1))
@@ -223,12 +226,6 @@ Should be one of `:white-split', `:modified' or `:default'")
   :init
   (setq company-idle-delay nil))
 
-(use-package exec-path-from-shell
-  :ensure t
-  :config
-  (when (memq window-system '(mac ns x))
-    (exec-path-from-shell-initialize)))
-
 (use-package shr
   :init
   (setq shr-use-fonts nil)
@@ -236,8 +233,13 @@ Should be one of `:white-split', `:modified' or `:default'")
 
 (use-package exec-path-from-shell
   :ensure t
+  :init
+  (setq exec-path-from-shell-arguments '("-l"))
   :config
   (when (memq window-system '(mac ns x))
+    (dolist (var '("SSH_AUTH_SOCK" "SSH_AGENT_PID" "GPG_AGENT_INFO" "LANG"
+                   "LC_CTYPE" "NIX_SSL_CERT_FILE" "NIX_PATH"))
+      (add-to-list 'exec-path-from-shell-variables var))
     (exec-path-from-shell-initialize)))
 
 (use-package browse-url
@@ -513,6 +515,8 @@ https://yannherklotz.com"))
                                  ("PROJ" . (:background "sea green" :weight bold))
                                  ("NO" . (:background "dark salmon"))
                                  ("KILL" . "pale green")))
+
+  (setq org-export-allow-bind-keywords t)
   :config
   (unbind-key "C-," org-mode-map))
 
@@ -634,12 +638,16 @@ https://yannherklotz.com"))
 (use-package boogie-friends
   :ensure t
   :init
-  (setq flycheck-inferior-dafny-executable "/Users/ymh/.vscode/extensions/dafny-lang.ide-vscode-3.0.4/out/resources/3.11.0/github/dafny/DafnyServer")
-  (setq dafny-verification-backend 'server)
+;;  (setq flycheck-inferior-dafny-executable "/Users/ymh/.local/dafny-4.0/DafnyServer")
+  (setq dafny-verification-backend nil)
   (setq boogie-friends-symbols-alist nil)
   :config
   (add-hook 'dafny-mode-hook
-            (lambda () (prettify-symbols-mode -1))))
+            (lambda () (prettify-symbols-mode -1)))
+  (add-hook 'dafny-mode-hook
+            (lambda ()
+              ;;(add-hook 'before-save-hook #'eglot-format 0 :local)
+              (setq fill-column 120))))
 
 (use-package direnv
   :if (executable-find "direnv")
@@ -923,10 +931,11 @@ https://yannherklotz.com"))
   (add-hook 'LaTeX-mode-hook
             (lambda ()
               (setq reftex-ref-style-default-list '("Default" "Cleveref"))))
-  (with-eval-after-load 'latex
-    (define-key LaTeX-mode-map
-      " "
-      #'ymh/electric-space)))
+  ;;(with-eval-after-load 'latex
+  ;;  (define-key LaTeX-mode-map
+  ;;    " "
+  ;;    #'ymh/electric-space))
+  )
 
 (use-package ox-hugo
   :ensure t)
@@ -978,12 +987,20 @@ https://yannherklotz.com"))
   :ensure t)
 
 (use-package eglot
-  :hook (scala-mode . eglot-ensure)
+  :hook ((scala-mode . eglot-ensure)
+         (dafny-mode . eglot-ensure))
+  :bind (:map eglot-mode-map
+              ("C-c f d" . eglot-format))
   :config
   (add-to-list 'eglot-server-programs
                '(prolog-mode
                  . ("swipl" "-g" "use_module(library(lsp_server))." "-g"
-                    "lsp_server:main" "-t" "halt" "--" "stdio"))))
+                    "lsp_server:main" "-t" "halt" "--" "stdio")))
+  (add-to-list 'eglot-server-programs
+               '(dafny-mode . ("dafny" "server"
+                               "--manual-lemma-induction"
+                               "--warn-missing-constructor-parentheses"
+                               "--warn-shadowing"))))
 
 (use-package elec-pair
   :config
@@ -998,6 +1015,9 @@ https://yannherklotz.com"))
 (use-package ox-texinfo
   :after org)
 
+(use-package ox-beamer
+  :after org)
+
 (use-package visual-fill-column
   :ensure t)
 
diff --git a/ymh-emacs/ymh-common.el b/ymh-emacs/ymh-common.el
index 3786016..09ebe08 100644
--- a/ymh-emacs/ymh-common.el
+++ b/ymh-emacs/ymh-common.el
@@ -45,9 +45,10 @@
 
 (defun ymh/electric-space ()
   (interactive)
-  (if (looking-back (sentence-end))
-      (insert "%\n")
-    (self-insert-command 1)))
+  (let ((sentence-end-double-space nil))
+    (if (looking-back (sentence-end))
+        (insert "\n")
+      (self-insert-command 1))))
 
 
 ;;; Stefan Monnier: It is the opposite of fill-paragraph.
-- 
cgit