[Agda] Emacs whitespace-mode

Andreas Abel andreas.abel at ifi.lmu.de
Thu Jan 24 18:51:47 CET 2019


I am using just

   (setq-default show-trailing-whitespace t)

Also, I am using Nisses automatic trailing-whitespace removal hook:


;; Draw tabs with the same color as trailing whitespace
(add-hook 'font-lock-mode-hook
   (lambda ()
     (when (member major-mode fix-whitespace-modes)
       (font-lock-add-keywords
         nil
         '(("\t" 0 'trailing-whitespace prepend))))))

;; Whitespace

(defvar fix-whitespace-modes
   '(text-mode agda2-mode haskell-mode literate-haskell-mode 
haskell-cabal-mode emacs-lisp-mode LaTeX-mode TeX-mode latex-mode 
plain-tex-mode tex-mode makefile-gmake-mode HTML-mode html-mode 
mhtml-mode bibtex-mode BibTeX-mode C-mode c++-mode java-mode 
haskell-cabal-mode lean-mode miniagda-mode python-mode sh-mode bnfc-mode 
nxml-mode rst-mode rust-mode conf-space-mode conf-colon-mode 
conf-unix-mode beluga-mode twelf-mode fstar-mode markdown-mode css-mode 
makefile-bsdmake-mode)
   "*Whitespace issues should be fixed when these modes are used.")

(add-hook 'before-save-hook
   (lambda nil
     (when (and (member major-mode fix-whitespace-modes)
                (not buffer-read-only))

       ;; Delete trailing whitespace.
       (delete-trailing-whitespace)

       ;; Insert a final newline character, if necessary.
       (save-excursion
         (save-restriction
           (widen)
           (unless (equal ?\n (char-before (point-max)))
             (goto-char (point-max))
             (insert "\n")))))))

On 2019-01-24 15:08, Matthew Daggitt wrote:
> Does anyone know of any existing incompatibilities with the emacs 
> `whitespace-mode` in `agda-mode`? I use to have it working but at some 
> point in the last couple of years it's stopped working. I have the 
> following code in my `.emacs` file:
> 
> (require 'whitespace)
> (setq whitespace-line-column 80) ;; limit line length
> (setq whitespace-style '(face lines-tail))
> (global-whitespace-mode +1)
> 
> and the highlighting works everywhere except in `.agda` files...
> Many thanks,
> Matthew
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


More information about the Agda mailing list