[Agda] Expanding literate Agda

[Andreas Abel]

Adding regular expressions to recognize more file extensions is easy for 
both the emacs-mode and Agda and the testsuite.

If we decide on non-hierarchical file extensions, we could accept .*agda 
which would subsume .agda, .lagda, .bird-agda, .md-agda, .latex-agda, ...

For hierarchical file extensions like .agda, .agda.tex, .agda.md it is 
only slightly more complicated.

Overloading file extensions is problematic already for plain-tex and 
latex, at least emacs sometimes gets confused, for instance if my latex 
file looks just like

$ cat icfp13-long.tex
% The long version contains the appendix with figures
% more proofs, and extra sections.

\newcommand{\LONGVERSION}[1]{#1}
\newcommand{\SHORTVERSION}[1]{}

\input{icfp13}

To see that this is LaTeX and not TeX, emacs would have to chase 
\input-statements, which of course it does not.  This might not readily 
apply to agda files, but I have a bad feeling about it.

On 13.10.2014 15:35, Pepijn Kokke wrote:
> If we use ".lagda" then currently agda-mode will be started and all Agda
> source is highlighted (and interactive, etc).
>
> If we use ".lagda.tex" then your editor will boot something like
> TeX-mode, where the TeX source is highlighted and the Agda source is
> (hopefully) untouched.
>
> As I see it, it's really a matter of preference.
>
> On 13 October 2014 14:08, Dominique Devriese
> <dominique.devriese at gmail.com <mailto:dominique.devriese at gmail.com>> wrote:
>
>     All,
>
>     2014-10-13 13:55 GMT+02:00 João Paulo Pizani Flor
>     <J.P.PizaniFlor at uu.nl <mailto: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 <http://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
>     <http://lagda.md>".
>
>      > Sorry for bikesheding,
>
>     Same here :).
>
>     Regards,
>     Dominique
>
>     P.S.: Kudos to the people doing the actual work ;)
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/