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

Alexandr Ruchkin 8 år siden opdateret 8 år siden 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.


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.

Kundesupport af UserEcho