Support for Agda (syntax, input unicode characters (\forall is for ∀, for example), integration with agda binary)

12 years ago • updated 12 years ago • 1

Agda is now possible to edit in emacs only, but Sublime seems to be perfect replacement for it.

Minimal list of features to support it is:

* Syntax (emacs doesn't support it by itself, only by grabbing some output from agda executable)

* Unicode symbols (when typing \forall, you get ∀, \-> is for → etc.)

* Grabbing output with highlighting from Agda

I'll try to make plugin myself, but I have no experience in it.

Vote

The way to highlight using agda executable is to invoke

agda --html some.agda -css=coloring.css -i include_dir_1 -i include_dir_2

It will produce all dependent modules in html with navigation.

This HTML possibly can be used to highlight active file in Sublime and to navigate on references.