[Agda] Expanding literate Agda

[Dominique Devriese]

All,

2014-10-13 13:55 GMT+02:00 João Paulo Pizani Flor <J.P.PizaniFlor at uu.nl>:
> But I also think "double extensions" should be avoided, and one reason for
> avoiding them is that external tools might get (very) confused.
>
> Text editor, standalone highlighters, plugins for CMS's, all of these tools
> that now assume that ".{,l}agda = Agda" and ".tex = TeX" will have to change
> their assumptions.
>
> It would be interesting, for example, that Literate Agda in LaTeX style is
> shown in a text editor with Agda highlighting. If "double extensions" are
> adopted, then a text editor might see the ".tex" extension, ignore what
> comes before, and show only TeX highlighting (ignoring the possibility of
> highlighting the Agda fragments).
> Even though we control the "official" Emacs mode, forcing these extension
> <-> filetype associations upstream to other tools would be too much effort.

I want to argue the opposite point :).  If we make sure, for example,
that literate Agda files with markdown support are still valid as
normal markdown files, similar to how lagda files are valid latex
files, then it makes sense to use extensions like "*.lagda.tex" or
"*.lagda.md".  The idea would be that editors (and other tools) that
don't know Agda will automatically treat these as "*.tex" or "*.md"
(i.e. use the standard highlighters/editing support for those
formats).  This would be a good thing because highlighting
"*.lagda.tex" as "*.tex" is better than highlighting "*.lagda" as
plaintext. The Agda-mode (which we control) and potentially other
editors which are aware of Agda (are there any so far?) and the
"lagda.*" idea could then treat them as "*.lagda.tex" or "*.lagda.md".

> Sorry for bikesheding,

Same here :).

Regards,
Dominique

P.S.: Kudos to the people doing the actual work ;)