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.
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.
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.