[Agda] Expanding literate Agda

[Pepijn Kokke]

>
> Note that inferring the file format also has to be implemented for the
> emacs-mode and all other front-ends to Agda.  I shortage of (willing)
> emacs-lisp programmers in our team, I'd like to avoid anything that
> complicates the emacs-mode.
>

The procedure to decide which format it is is relatively simple, but I too
feel that it shouldn't be implemented in the agda-mode. Since agda-mode
already needs an instance of Agda running in order to highlight files, the
procedure could simply be exposed through the interactive mode.

If the format is decided to be LaTeX, agda-mode could call its (internal?)
LaTeX highlighter. If it isn't, we could rule that the host language is
simply *not* highlighted---or we could try to call an external highlighter.
I'm hoping that most highlighters wouldn't touch a nested code block anyway.

All in all I don't think that the changes would be that great. At the
moment it already seems to work fine (with the host language not being
highlighted if it's not LaTeX) but I feel this is probably due to the
highlighter not finding anything to highlight.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141013/171b6e4f/attachment.html