Better Org-mode support for Literate Agda

Introduction

An Emacs major mode for editing Agda code embedded in Org files (.lagda.org files.) See the Agda manual for more information.

An older version of this support is documented in a blog post. The current version is a complete departure, motivated by

• the support in recent Agda versions (> 2.6) for literate files with .lagda.org extensions, and
• the ability to work in multiple Emacs modes at once via the Polymode package.

Package header

;;; org-agda-mode.el --- Major mode for working with literate Org Agda files
;;; -*- lexical-binding: t

;;; Commentary:

;; A Major mode for editing Agda code embedded in Org files (.lagda.org files.)
;; See the Agda manual for more information:
;; https://agda.readthedocs.io/en/v2.6.1/tools/literate-programming.html#literate-org

;;; Code:

Installation

Simply place org-agda-mode.el in your Emacs load path, and add

(require 'org-agda-mode)

to your Emacs initialisation file.

Alternatively, if you use straight.el and use-package, then this package can be installed by adding the following to your emacs configuration.

(use-package polymode)
(use-package org-agda-mode
  :straight (:host github
		   :repo "alhassy/org-agda-mode"
		   :branch "master"
		   :files ("org-agda-mode.el")
		   )
  )

Background

Polymode

Polymode allows us to use more than one major mode in a buffer, something usually impossible in Emacs. Note there do exist several other solutions for this, such as MMM; Polymode seemed the best candidate for what I want during my (admittedly rather brief) search for solutions.

Read the docs!

Prerequisite packages

(require 'polymode)
(require 'agda2-mode)

Customisations

(defgroup org-agda-mode nil
  "org-agda-mode customisations"
  :group 'languages)

Naturally, users will often want to use Agda input mode to enter unicode characters in their literate documentation. Do note that it’s also possible to enable this input mode globally in your Emacs init.

(defcustom use-agda-input t
  "Whether to use Agda input mode in non-Agda parts of the file."
  :group 'org-agda-mode
  :type 'boolean)

Org-Agda mode definition

Org is our hostmode.

(define-hostmode poly-org-agda-hostmode
  :mode 'org-mode
  :keep-in-mode 'host)

Agda is our inner mode, delimited by Org source blocks.

(define-innermode poly-org-agda-innermode
  :mode 'agda2-mode
  :head-matcher "#\\+begin_src agda2"
  :tail-matcher "#\\+end_src"
  ;; Keep the code block wrappers in Org mode, so they can be folded, etc.
  :head-mode 'org-mode
  :tail-mode 'org-mode
  ;; Disable font-lock-mode, which interferes with Agda annotations,
  ;; and undo the change to indent-line-function Polymode makes.
  :init-functions '((lambda (_) (font-lock-mode 0))
                    (lambda (_) (setq indent-line-function #'indent-relative))))

Now we define the polymode using the above host and inner modes.

(define-polymode org-agda-mode
  :hostmode 'poly-org-agda-hostmode
  :innermodes '(poly-org-agda-innermode)
  (when use-agda-input (set-input-method "Agda")))

Prevent Agda from applying annotations to the literate Org portion

Agda’s highlighting mode makes use of annotate to apply syntax highlighting throughout the buffer, including the literate portion, which agda2-highlight identifies as “background”. Older versions of Agda would highlight the background using font-lock-comment-face (so, making them the same colour as comments). Newer versions (since this commit) simply apply Emacs’ default face.

Since we’re using Org mode for the literate portion, we don’t want Agda to apply any annotation there. We can achieve this by simply removing the setting for background from the Agda highlight faces attribute list.

(assq-delete-all 'background agda2-highlight-faces)

There is a greater conflict between annotate and font-lock that we need to fix.

Automatically use org-agda-mode for .lagda.org files

Finally, add our new mode to the auto mode list.

;;;###autoload
(add-to-list 'auto-mode-alist '("\\.lagda.org" . org-agda-mode))

Package footer

(provide 'org-agda-mode)
;;; org-agda-mode ends here

Improvements

• Enable Agda loading, and more generally all the agda keybindings, anywhere in .lagda.org files.
  • At least the important ones that don’t obviously clash with Org bindings.
  • I’ve tried loading via M-x agda2-load from the Org portion, and it works (yay!), but it loses the Agda syntax highlighting?
• To enable monolith .lagda.org files (large literate files which tangle several individual clean source files), we need a way to strip one level of indentation after tangling.
  • Actually it’s not needed; Agda does allow the contents of the toplevel module (so, the remainder of the file) to be indented; but it breaks convention.

Documentation

• Discover the exact version of Agda that added support for interactive programming in .lagda.org files.