/jonprl-mode

An Emac major mode for writing JonPRL code

Primary LanguageEmacs Lisp

JonPRL Mode for Emacs

This is a simple major mode for the JonPRL implementation of computational type theory.

Features:

  • Completion for keywords, tactics, and operators
  • Dynamic generation of yasnippets for each operator
  • IMenu
  • Simple syntax highlighting, generated from JonPRL’s notion of defined operators
  • Eldoc, for showing summaries of tactics or operators in the minibuffer
  • Run JonPRL in compilation mode (bound to C-c C-l)
  • View JonPRL’s elaborated development (bound to C-c C-c)

To install, arrange for jonprl-mode.el to be on your load-path and then require it.

You may need to customize jonprl-path if the jonprl binary isn’t already on your PATH.

Yasnippet integration

jonprl-mode gets a list of defined operators from JonPRL and uses them to dynamically populate the Yasnippet snippet list. To enable this feature, add yas-minor-mode to your jonprl-mode-hook.

If you use this, then you probably want to set yas-triggers-in-field to t to enable recursive expansion of operators. This gives an experience reminiscent of the Nuprl structure editor.

Dynamic highlighting of tactics

jonprl-mode reads the list of tactics to highlight from JonPRL itself. If you do something that changes the list of available tactics, restart jonprl-mode with M-x jonprl-mode to re-read them.