diff --git a/src/data/emacs-mode/agda-input.el b/src/data/emacs-mode/agda-input.el
index 473c8674..9cb09a04 100644
--- a/src/data/emacs-mode/agda-input.el
+++ b/src/data/emacs-mode/agda-input.el
@@ -53,11 +53,11 @@ removing all space and newline characters."
 ;; Functions used to tweak translation pairs
 
 (defun agda-input-compose (f g)
-  "\x -> concatMap F (G x)"
+  "λ x -> concatMap F (G x)"
     (lambda (x) (agda-input-concat-map f (funcall g x))))
 
 (defun agda-input-or (f g)
-  "\x -> F x ++ G x"
+  "λ x -> F x ++ G x"
     (lambda (x) (append (funcall f x) (funcall g x))))
 
 (defun agda-input-nonempty ()
@@ -340,6 +340,37 @@ order for the change to take effect."
   ("bx" . ("⊠"))
   ("b." . ("⊡"))
 
+  ;; APL boxed operators
+
+  ("box="       . ("⌸"))
+  ("box?"       . ("⍰"))
+  ("box'"       . ("⍞"))
+  ("box:"       . ("⍠"))
+  ("box/"       . ("⍁"))
+  ("box\\"      . ("⍂"))
+  ("box<"       . ("⍃"))
+  ("box>"       . ("⍄"))
+  ("boxo"       . ("⌻"))
+  ("boxO"       . ("⌼"))
+
+  ("boxcomp"    . ("⌻"))
+  ("boxcircle"  . ("⌼"))
+  ("boxeq"      . ("⌸"))
+  ("boxneq"     . ("⍯"))
+  ("boxeqn"     . ("⍯"))
+
+  ("boxl"       . ("⍇"))
+  ("boxr"       . ("⍈"))
+  ("boxu"       . ("⍐"))
+  ("boxd"       . ("⍗"))
+
+  ("boxdi"      . ("⌺"))
+  ("boxdiv"     . ("⌹"))
+  ("boxwedge"   . ("⍓"))
+  ("boxvee"     . ("⍌"))
+  ("boxdelta"   . ("⍍"))
+  ("boxnabla"   . ("⍔"))
+
   ;; Various symbols.
 
   ("integral" . ,(agda-input-to-string-list "∫∬∭∮∯∰∱∲∳"))
diff --git a/src/data/emacs-mode/agda2-highlight.el b/src/data/emacs-mode/agda2-highlight.el
index 9fcea0e6..73cbcdd5 100644
--- a/src/data/emacs-mode/agda2-highlight.el
+++ b/src/data/emacs-mode/agda2-highlight.el
@@ -58,24 +58,6 @@ If the face does not exist, then it is created first."
                       :font           'unspecified)
   (eval `(set-face-attribute face nil ,@attrs)))
 
-(defvar agda2-highlight-face-attributes-list
-  '(:family :width :height :weight :slant :foreground :background
-            :inverse-video :stipple :underline :overline :strike-through
-            :inherit :box :font)
-  "The attributes considered by `agda2-highlight-face-attributes'.")
-
-(defun agda2-highlight-face-attributes (face)
-  "The names and values of all attributes in FACE.
-Only the attributes in `agda2-highlight-face-attributes-list' are
-considered. The attributes are returned in a flat list of the
-form (name1 value1 name2 value2...)."
-  (apply 'append
-         (mapcar (lambda (attr)
-                   (let ((val (face-attribute face attr)))
-                     (if (member val '(unspecified nil)) '()
-                       (list attr (if (symbolp val) `',val val)))))
-                 agda2-highlight-face-attributes-list)))
-
 (defun agda2-highlight-set-faces (variable group)
   "Set all Agda faces according to the value of GROUP.
 Also sets the default value of VARIABLE to GROUP."
@@ -146,71 +128,49 @@ Also sets the default value of VARIABLE to GROUP."
              :background "light blue")))
          ((equal group 'default-faces)
           (list (cons 'agda2-highlight-keyword-face
-                      (agda2-highlight-face-attributes
-                       font-lock-keyword-face))
+                      (list :inherit font-lock-keyword-face))
                 (cons 'agda2-highlight-string-face
-                      (agda2-highlight-face-attributes
-                       font-lock-string-face))
+                      (list :inherit font-lock-string-face))
                 (cons 'agda2-highlight-number-face
-                      (agda2-highlight-face-attributes
-                       font-lock-constant-face))
+                      (list :inherit font-lock-constant-face))
                 (cons 'agda2-highlight-symbol-face
-                      (agda2-highlight-face-attributes
-                       font-lock-keyword-face))
+                      (list :inherit font-lock-keyword-face))
                 (cons 'agda2-highlight-primitive-type-face
-                      (agda2-highlight-face-attributes
-                       font-lock-keyword-face))
+                      (list :inherit font-lock-keyword-face))
                 (cons 'agda2-highlight-bound-variable-face
-                      (agda2-highlight-face-attributes
-                       font-lock-variable-name-face))
+                      (list :inherit font-lock-variable-name-face))
                 (cons 'agda2-highlight-generalizable-variable-face
-                      (agda2-highlight-face-attributes
-                       font-lock-variable-name-face))
+                      (list :inherit font-lock-variable-name-face))
                 (cons 'agda2-highlight-inductive-constructor-face
-                      (agda2-highlight-face-attributes
-                       font-lock-type-face))
+                      (list :inherit font-lock-type-face))
                 (cons 'agda2-highlight-coinductive-constructor-face
-                      (agda2-highlight-face-attributes
-                       font-lock-type-face))
+                      (list :inherit font-lock-type-face))
                 (cons 'agda2-highlight-datatype-face
-                      (agda2-highlight-face-attributes
-                       font-lock-type-face))
+                      (list :inherit font-lock-type-face))
                 (cons 'agda2-highlight-field-face
-                      (agda2-highlight-face-attributes
-                       font-lock-variable-name-face))
+                      (list :inherit font-lock-variable-name-face))
                 (cons 'agda2-highlight-function-face
-                      (agda2-highlight-face-attributes
-                       font-lock-function-name-face))
+                      (list :inherit font-lock-function-name-face))
                 (cons 'agda2-highlight-module-face
-                      (agda2-highlight-face-attributes
-                       font-lock-type-face))
+                      (list :inherit font-lock-type-face))
                 (cons 'agda2-highlight-postulate-face
-                      (agda2-highlight-face-attributes
-                       font-lock-type-face))
+                      (list :inherit font-lock-type-face))
                 (cons 'agda2-highlight-primitive-face
-                      (agda2-highlight-face-attributes
-                       font-lock-constant-face))
+                      (list :inherit font-lock-constant-face))
                 (cons 'agda2-highlight-macro-face
-                      (agda2-highlight-face-attributes
-                       font-lock-function-name-face))
+                      (list :inherit font-lock-function-name-face))
                 (cons 'agda2-highlight-record-face
-                      (agda2-highlight-face-attributes
-                       font-lock-variable-name-face))
+                      (list :inherit font-lock-variable-name-face))
                 (cons 'agda2-highlight-dotted-face
-                      (agda2-highlight-face-attributes
-                       font-lock-variable-name-face))
+                      (list :inherit font-lock-variable-name-face))
                 (cons 'agda2-highlight-operator-face
-                      (agda2-highlight-face-attributes
-                       font-lock-function-name-face))
+                      (list :inherit font-lock-function-name-face))
                 (cons 'agda2-highlight-error-face
-                      (agda2-highlight-face-attributes
-                       font-lock-warning-face))
+                      (list :inherit font-lock-warning-face))
                 (cons 'agda2-highlight-typechecks-face
-                      (agda2-highlight-face-attributes
-                       font-lock-type-face))
+                      (list :inherit font-lock-type-face))
                 (cons 'agda2-highlight-typechecking-face
-                      (agda2-highlight-face-attributes
-                       font-lock-preprocessor-face)))))))
+                      (list :inherit font-lock-preprocessor-face)))))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Faces
diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el
index 1c613836..3bd1da96 100644
--- a/src/data/emacs-mode/agda2-mode-pkg.el
+++ b/src/data/emacs-mode/agda2-mode-pkg.el
@@ -1,3 +1,3 @@
-(define-package "agda2-mode" "2.6.3"
+(define-package "agda2-mode" "2.6.4"
   "interactive development for Agda, a dependently typed functional programming language"
-  '((emacs "24.3") (annotation "1.0") (eri "1.0")))
+  '((emacs "24.3"))) ;; dep defs for `annotation.el` and `eri.el` are not required if they are packaged together
diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el
index a9ad946e..85ce62a1 100644
--- a/src/data/emacs-mode/agda2-mode.el
+++ b/src/data/emacs-mode/agda2-mode.el
@@ -31,7 +31,7 @@
 
 ;;; Code:
 
-(defvar agda2-version "2.6.3"
+(defvar agda2-version "2.6.4"
   "The version of the Agda mode.
 Note that the same version of the Agda executable must be used.")
 
@@ -93,7 +93,7 @@ Or possibly (let* VARBIND (labels FUNCBIND BODY...))."
   :group 'agda2)
 
 (defcustom agda2-program-args
-  '("--disable-backend")                    ; so that it doesn't complain about mixing backend with frontend
+  '("--disable-backend")       ; so that it doesn't complain about mixing backend with frontend
   "Command-line arguments given to the Agda executable (one per string).
 
 Note: Do not give several arguments in the same string.
@@ -103,7 +103,7 @@ argument, and does not need to be listed here."
   :type '(repeat string)
   :group 'agda2)
 
-(defvar agda2-backends '("AGDA2HS")
+(defvar agda2-backends '("AGDA2HS" "GHC" "GHCNoMain" "JS" "LaTeX" "QuickLaTeX")
   "Compilation backends.")
 
 (defcustom agda2-backend
@@ -265,13 +265,13 @@ constituents.")
   "Table of commands, used to build keymaps and menus.
 Each element has the form (CMD &optional KEYS WHERE DESC) where
 CMD is a command; KEYS is its key binding (if any); WHERE is a
-list which should contain 'local if the command should exist in
-the goal menu and 'global if the command should exist in the main
+list which should contain \\='local if the command should exist in
+the goal menu and \\='global if the command should exist in the main
 menu; and DESC is the description of the command used in the
 menus.")
 
 (defvar agda2-mode-map
-  (let ((map (make-sparse-keymap "Agda mode")))
+  (let ((map (make-sparse-keymap "Agda2Hs mode")))
     (define-key map [menu-bar Agda]
       (cons "Agda2Hs" (make-sparse-keymap "Agda2Hs")))
     (define-key map [down-mouse-3]  'agda2-popup-menu-3)
@@ -534,7 +534,7 @@ process."
 Sends the list of strings ARGS to the Agda2 interpreter, waits
 for output and executes the responses, if any.
 
-If SAVE is 'save, then the buffer is saved first.
+If SAVE is \\='save, then the buffer is saved first.
 
 If HIGHLIGHT is non-nil, then the buffer's syntax highlighting
 may be updated. This is also the case if the Agda process is
@@ -763,13 +763,13 @@ The user input is computed as follows:
   contains whitespace, then the input is taken from the
   minibuffer. In this case WANT is used as the prompt string.
 
-* Otherwise (including if WANT is 'goal) the goal contents are
+* Otherwise (including if WANT is \\='goal) the goal contents are
   used.
 
 If the user input is not taken from the goal, then an empty goal
 range is given.
 
-If SAVE is 'save, then the buffer is saved just before the
+If SAVE is \\='save, then the buffer is saved just before the
 command is sent to Agda (if it is sent)."
   (cl-multiple-value-bind (o g) (agda2-goal-at (point))
     (unless g (error "For this command, please place the cursor in a goal"))
@@ -896,8 +896,8 @@ of new goals."
  (agda2-goal-cmd "Cmd_autoOne" 'save 'goal))
 
 (defun agda2-autoAll ()
-  (interactive)
   "Solves all goals by simple proof search."
+  (interactive)
   (agda2-go nil nil 'busy t "Cmd_autoAll")
 )
 
@@ -1953,7 +1953,7 @@ the argument is a positive number, otherwise turn it off."
 
 (defun agda2-get-agda-program-versions ()
   "Get \"version strings\" of executables starting with
-'agda-mode' in current path."
+\\='agda2hs-mode\\=' in current path."
   (delete-dups
    (mapcar (lambda (path)
              ;; strip 'agda2hs-mode' prefix