Janitorial Changes to agda-mode (#6536)

* agda-mode: Add a basic .dir-locals.el file for agda2-mode

* agda-mode: Remove hanging parentheses

* agda-mode: Set the input method just for the current agda2-mode buffer

* agda-mode: Use dolist in agda2-goal-overlay

* agda-mode: Have agda2-char-quote return strings

* agda-mode: Use sharp-quotes where applicable

* agda2-mode.el (agda2-infer-type-maybe-toplevel): Sharp-quote 'agda2-infer-type'.
(agda2-solveAll-action): Sharp-quite 'agda2-solve-action'.
(agda2-compute-normalised-maybe-toplevel): Sharp quote
'agda2-compute-normalised' and 'agda2-compute-normalised-toplevel'.

Sharp-quoting functions indicates that a symbol should have a bound
function slot, and that the byte compiler should check if this is the
case, otherwise emit a warning.

* agda-mode: Fix checkdoc and byte-compiler issues

* agda-mode: Drop the 'agda2-let' macro

* agda-mode: Add .agdai files to 'completion-ignored-extensions'

* agda-mode: Remove compatibility code for versions older than GNU Emacs 25.1

* agda-mode: Replace 'agda2--case' with 'pcase'

* agda-mode: Fix minor stylistic issues

* agda-mode: Prefer 'defvar-local' over 'make-variable-buffer-local'

* agda-mode: Prefer 'setq-local' over 'make-local-variable'

* agda-mode: Flatten 'agda2-get-agda-program-versions'

* agda-mode: Use 'cl-remove-if-not' instead of 'cl-mapcan'

* agda-mode: Prefer member functions over (or (eq...) ...)

* agda-mode: Avoid using 'equal' where unnecessary

'Equal' is used for structural equality, which is not necessary for
atomic objects like symbol or numbers.  In that case referential
equality, 'eq' or a specialised procedure like 'zerop' or 'null' is
preferred.

* agda-mode: Add a custom setter to 'agda2-mode-abbrevs-use-defaults'

* agda-mode: Replace 'agda2-command-table' with regular maps

* agda-mode: Replace agda2-queue with a regular buffer

* agda-mode: Use more consistent outlines in agda2-mode.el

* agda-mode: Use more consistent outlines in agda2-highlight.el

* agda-mode: Use more consistent outlines in agda2-input.el

* agda-mode: Use 'with-silent-modifications'

* agda-mode: Only use exec-path as a function if fboundp

* agda-mode: Modify 'file-coding-system-alist' directly

* agda-mode: Move add-to-list autoloads to agda2.el to avoid duplication

* agda-mode: Use a "hidden name" for the Agda process buffer

* agda-mode: Use 'apply' instead of 'eval'

It is not necessary to use 'eval' to invoke a function with an
argument list of unknown length.

* agda-mode: Add a "Code" header to agda2.el

* agda-mode: Do not disable cl-function warnings

* agda-mode: Enable debug-on-error for agda-mode when compiling

* agda-mode: Use 'barf-if-buffer-read-only' instead of checking manually

* agda-mode: Avoid usage of deprecated 'window-system' variable

* agda-mode: Do not control evaluation using buffer-local values

* agda-mode: Further simplify process filter

This change builds on c7492c0,
dropping the need for any queue (of string or a buffer), by inserting
the process output directly into the process buffer and operating on
thereon.  We avoid the overhead of consing lists and strings, while
simplifying the logic by relying more on Lisp primitives.

src/agda-mode/Main.hs

@@ -264,8 +264,8 @@ compileElispFiles = do
       , "--batch"                -- 'batch' implies 'no-init-file' but not 'no-site-file'.
       , "--eval"
       , "(progn \
+           \(setq debug-on-error t) \
            \(setq byte-compile-error-on-warn t) \
-           \(byte-compile-disable-warning 'cl-functions) \
            \(batch-byte-compile))"
       , f
       ]

src/data/emacs-mode/.dir-locals.el

@@ -0,0 +1,6 @@
+;;; Directory Local Variables         -*- no-byte-compile: t; -*-
+;;; For more information see (info "(emacs) Directory Variables")
+
+((emacs-lisp-mode
+  (show-trailing-whitespace . t)
+  (indent-tabs-mode . nil)))

src/data/emacs-mode/agda-input.el

@@ -26,8 +26,7 @@
 ;; that with-temp-buffer is used below whenever buffer-local state is
 ;; modified.
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Utility functions
+;;;; Utility functions
 
 (defun agda-input-concat-map (f xs)
   "Concat (map F XS)."
@@ -49,8 +48,7 @@ removing all space and newline characters."
       (setq seq (cons (+ from i) seq)))
     (concat (nreverse seq))))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Functions used to tweak translation pairs
+;;;; Functions used to tweak translation pairs
 
 (defun agda-input-compose (f g)
   "λ x -> concatMap F (G x)"
@@ -111,8 +109,7 @@ This suffix is dropped."
      (agda-input-drop-end (length suffix))
      (agda-input-suffix suffix)))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Customization
+;;;; Customization
 
 ;; The :set keyword is set to 'agda-input-incorporate-changed-setting
 ;; so that the input method gets updated immediately when users
@@ -1356,8 +1353,7 @@ methods."
   :type '(repeat (cons (string :tag "Key sequence")
                        (repeat :tag "Translations" string))))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Inspecting and modifying translation maps
+;;;; Inspecting and modifying translation maps
 
 (defun agda-input-get-translations (qp)
   "Return a list containing all translations from the Quail
@@ -1402,8 +1398,7 @@ a list of such pairs."
      (if fun (agda-input-concat-map fun trans)
        trans))))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Setting up the input method
+;;;; Setting up the input method
 
 (defun agda-input-setup ()
   "Set up the Agda input method based on the customisable
@@ -1438,8 +1433,5 @@ Suitable for use in the :set field of `defcustom'."
 
 (agda-input-setup)
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Administrative details
-
 (provide 'agda-input)
 ;;; agda-input.el ends here

src/data/emacs-mode/agda2-abbrevs.el

@@ -77,27 +77,35 @@
   ("oi"  "open import "))
   "Abbreviations defined by default in the Agda mode.")
 
+(defvar agda2-mode-abbrev-table nil
+  "Agda mode abbrev table.")
+
+(defvar agda2-mode-abbrevs-use-defaults)
+(defun agda2-mode-abbrevs-use-defaults ()
+  "Load or disable Agda abbrevs."
+  (define-abbrev-table
+    'agda2-mode-abbrev-table
+    (and (bound-and-true-p agda2-mode-abbrevs-use-defaults)
+         (mapcar (lambda (abbrev)
+                   (append abbrev
+                           (make-list (- 4 (length abbrev)) nil)
+                           '((:system t))))
+                 agda2-abbrevs-defaults))))
+
 (defcustom agda2-mode-abbrevs-use-defaults nil
   "If non-nil include the default Agda mode abbrevs in `agda2-mode-abbrev-table'.
 The abbrevs are designed to be expanded explicitly, so users of `abbrev-mode'
 probably do not want to include them.
 
 Restart Emacs in order for this change to take effect."
   :group 'agda2
+  :set (lambda (sym val)
+         (custom-set-default sym val)
+         (agda2-mode-abbrevs-use-defaults))
   :type '(choice (const :tag "Yes" t)
                  (const :tag "No" nil)))
 
-(defvar agda2-mode-abbrev-table nil
-  "Agda mode abbrev table.")
-
-(define-abbrev-table
-  'agda2-mode-abbrev-table
-  (if agda2-mode-abbrevs-use-defaults
-      (mapcar (lambda (abbrev)
-                (append abbrev
-                        (make-list (- 4 (length abbrev)) nil)
-                        '((:system t))))
-              agda2-abbrevs-defaults)))
+(agda2-mode-abbrevs-use-defaults)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Administrative details

src/data/emacs-mode/agda2-highlight.el

@@ -1,11 +1,14 @@
-;;; agda2-highlight.el --- Syntax highlighting for Agda (version ≥ 2)
+;;; agda2-highlight.el --- Syntax highlighting for Agda -*- lexical-binding: t; -*-
+
+;; URL: https://github.com/agda/agda/tree/master/src/data/emacs-mode
 ;; SPDX-License-Identifier: MIT License
 
 ;;; Commentary:
 
-;; Code to apply syntactic highlighting to Agda source code. This uses
-;; Agda's own annotations to figure out what is what, so the parsing
-;; is always done correctly, but highlighting is not done on the fly.
+;; Code to apply syntactic highlighting to Agda source code.  This
+;; uses Agda's own annotations to figure out what is what, so the
+;; parsing is always done correctly, but highlighting is not done on
+;; the fly.
 
 ;;; Code:
 
@@ -28,13 +31,12 @@ that is currently being type-checked."
 
 (defun agda2-highlight-level nil
   "Formats the highlighting level in a Haskelly way."
-  (cond ((equal agda2-highlight-level 'none)            "None")
-        ((equal agda2-highlight-level 'non-interactive) "NonInteractive")
-        ((equal agda2-highlight-level 'interactive)     "Interactive")
-        (t                                              "None")))
+  (cond ((eq agda2-highlight-level 'none)            "None")
+        ((eq agda2-highlight-level 'non-interactive) "NonInteractive")
+        ((eq agda2-highlight-level 'interactive)     "Interactive")
+        (t                                           "None")))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Functions for setting faces
+;;;; Functions for setting faces
 
 (defun agda2-highlight-set-face-attribute (face attrs)
   "Reset (globally) all attributes of the face FACE according to ATTRS.
@@ -56,7 +58,7 @@ If the face does not exist, then it is created first."
                       :inherit        'unspecified
                       :box            'unspecified
                       :font           'unspecified)
-  (eval `(set-face-attribute face nil ,@attrs)))
+  (apply #'set-face-attribute face nil attrs))
 
 (defun agda2-highlight-set-faces (variable group)
   "Set all Agda faces according to the value of GROUP.
@@ -172,8 +174,7 @@ Also sets the default value of VARIABLE to GROUP."
                 (cons 'agda2-highlight-typechecking-face
                       (list :inherit font-lock-preprocessor-face)))))))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Faces
+;;;; Faces
 
 (defcustom agda2-highlight-face-groups nil
   "Colour scheme used in Agda buffers.
@@ -526,15 +527,13 @@ The aspects currently recognised are the following:
                            variables.
 `unsolvedmeta'           Unsolved meta variables.")
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Variables
+;;;; Variables
 
 (defvar agda2-highlight-in-progress nil
   "If nil, then highlighting annotations are not applied.")
 (make-variable-buffer-local 'agda2-highlight-in-progress)
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Functions
+;;;; Functions
 
 (defun agda2-highlight-setup nil
   "Set up the `annotation' library for use with `agda2-mode'."
@@ -589,8 +588,6 @@ removed."
        ; Ignore read-only status, otherwise this function may fail.
     (annotation-remove-annotations token-based)))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Administrative details
 
 (provide 'agda2-highlight)
 ;;; agda2-highlight.el ends here