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.