diff --git a/math/hs-Agda/Makefile b/math/hs-Agda/Makefile
index 05efa5aacf69..bb6ed72f2ce6 100644
--- a/math/hs-Agda/Makefile
+++ b/math/hs-Agda/Makefile
@@ -1,100 +1,101 @@
 PORTNAME=	Agda
 PORTVERSION=	2.6.3
+PORTREVISION=	1
 CATEGORIES=	math haskell
 
 MAINTAINER=	haskell@FreeBSD.org
 COMMENT=	Dependently typed functional programming language and proof assistant
 WWW=		https://wiki.portal.chalmers.se/agda/
 
 LICENSE=	UNKNOWN
 LICENSE_NAME=	custom
 LICENSE_FILE=	${WRKSRC}/LICENSE
 LICENSE_PERMS=	dist-mirror no-dist-sell pkg-mirror no-pkg-sell auto-accept
 
 BROKEN_i386=	Compiler goes out of memory
 
 BUILD_DEPENDS=	emacs:editors/emacs
 
 USES=		cabal
 
 USE_LOCALE=	en_US.UTF-8
 
 USE_CABAL=	OneTuple-0.4.1.1 \
 		QuickCheck-2.14.2 \
 		STMonadTrans-0.4.6_1 \
 		StateVar-1.2.2 \
 		aeson-2.1.2.1_1 \
 		alex-3.2.7.1 \
 		assoc-1.0.2_3 \
 		async-2.2.4_2 \
 		attoparsec-0.14.4_3 \
 		base-compat-0.12.2 \
 		base-compat-batteries-0.12.2 \
 		base-orphans-0.8.8.2 \
 		bifunctors-5.5.15 \
 		blaze-builder-0.4.2.2_1 \
 		blaze-html-0.9.1.2_2 \
 		blaze-markup-0.8.2.8_3 \
 		boxes-0.1.5 \
 		case-insensitive-1.2.1.0 \
 		comonad-5.0.8_1 \
 		contravariant-1.5.5 \
 		data-array-byte-0.1.0.1_1 \
 		data-fix-0.3.2_3 \
 		data-hash-0.2.0.1 \
 		distributive-0.6.2.1_1 \
 		dlist-1.0 \
 		edit-distance-0.2.2.1_1 \
 		equivalence-0.4.1 \
 		generically-0.1.1 \
 		gitrev-1.3.1 \
 		happy-1.20.1.1 \
 		hashable-1.4.2.0 \
 		indexed-traversable-0.1.2_2 \
 		indexed-traversable-instances-0.1.1.2 \
 		integer-logarithms-1.0.3.1_4 \
 		monad-control-1.0.3.1 \
 		murmur-hash-0.1.0.10 \
 		network-uri-2.6.4.2 \
 		parallel-3.2.2.0_5 \
 		primitive-0.8.0.0 \
 		random-1.2.1.1 \
 		regex-base-0.94.0.2_1 \
 		regex-tdfa-1.3.2 \
 		scientific-0.3.7.0_4 \
 		semialign-1.2.0.1_3 \
 		semigroupoids-5.3.7_1 \
 		split-0.2.3.5 \
 		splitmix-0.1.0.4_2 \
 		strict-0.4.0.1_4 \
 		tagged-0.8.7 \
 		text-short-0.1.5_1 \
 		th-abstraction-0.5.0.0 \
 		th-compat-0.1.4_2 \
 		these-1.1.1.1_6 \
 		time-compat-1.9.6.1_4 \
 		transformers-base-0.4.6 \
 		transformers-compat-0.7.2 \
 		unordered-containers-0.2.19.1_1 \
 		uri-encode-1.5.0.7_2 \
 		utf8-string-1.0.2 \
 		uuid-types-1.0.5_3 \
 		vector-0.13.0.0_3 \
 		vector-hashtables-0.1.1.2 \
 		vector-stream-0.1.0.0_2 \
 		witherable-0.4.2_4 \
 		zlib-0.6.3.0_1
 
 CABAL_EXECUTABLES=	agda-mode agda
 CABAL_WRAPPER_SCRIPTS=	${CABAL_EXECUTABLES}
 agda_DATADIR_VARS=	Agda
 agda-mode_DATADIR_VARS=	Agda
 
 post-install:
 	${SETENV} Agda_datadir=${WRKSRC}/src/data ${STAGEDIR}${PREFIX}/libexec/cabal/agda-mode compile
 	find ${WRKSRC}/src/data/lib/prim/Agda -name '*.agda' -exec ${SETENV} Agda_datadir=${WRKSRC}/src/data ${STAGEDIR}${PREFIX}/libexec/cabal/agda {} \;
 	${MKDIR} ${STAGEDIR}${DATADIR}/lib/prim/Agda
 	cd ${WRKSRC}/src/data && ${COPYTREE_SHARE} lib ${STAGEDIR}${DATADIR}
 	cd ${WRKSRC}/src/data && ${COPYTREE_SHARE} emacs-mode ${STAGEDIR}${DATADIR}
 
 .include <bsd.port.mk>
diff --git a/math/hs-Agda/files/patch-src_data_emacs-mode_agda2-mode.el b/math/hs-Agda/files/patch-src_data_emacs-mode_agda2-mode.el
new file mode 100644
index 000000000000..8bca8c0cc516
--- /dev/null
+++ b/math/hs-Agda/files/patch-src_data_emacs-mode_agda2-mode.el
@@ -0,0 +1,57 @@
+https://github.com/agda/agda/pull/6735
+
+--- src/data/emacs-mode/agda2-mode.el.orig	2001-09-09 01:46:40 UTC
++++ src/data/emacs-mode/agda2-mode.el
+@@ -261,8 +261,8 @@ CMD is a command; KEYS is its key binding (if any); WH
+   "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.")
+ 
+@@ -530,7 +530,7 @@ for output and executes the responses, if any.
+ 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
+@@ -759,13 +759,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"))
+@@ -893,7 +893,6 @@ of new goals."
+ 
+ (defun agda2-autoAll ()
+   (interactive)
+-  "Solves all goals by simple proof search."
+   (agda2-go nil nil 'busy t "Cmd_autoAll")
+ )
+ 
+@@ -1949,7 +1948,7 @@ the argument is a positive number, otherwise turn it o
+ 
+ (defun agda2-get-agda-program-versions ()
+   "Get \"version strings\" of executables starting with
+-'agda-mode' in current path."
++\\='agda-mode' in current path."
+   (delete-dups
+    (mapcar (lambda (path)
+              ;; strip 'agda-mode' prefix