[Agda] Expanding literate Agda

[Andreas Abel]

I am against overloading a file extension like .lagda.  I do not see why 
it is necessary.  Since file extensions can be longer than 3 characters 
(as it was in good old DOS times), we do not have to be frugal.

.lagda should be reserved for latex-agda, and we can have new extensions 
for other literate Agda variants.

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.

 From https://code.google.com/p/agda/issues/detail?id=508#c10
   I would like to see different flavors of literate Agda have distinct 
file extension, such that no guessing is needed.  Maybe:

.agda.tex -- for LaTeX-style
.agda.md -- for markdown style
.agda.txt  -- for Bird-style

I am not sure if having a double extension is a good idea, though.  Maybe

.agda-tex
.agda-md
.agda-txt

instead?

In general, agda-* could be reserved for a version of literate Agda.

Cheers,
Andreas

On 13.10.2014 06:55, Ulf Norell wrote:
> I'm also in favour of the first solution. Using double extensions is not
> really standard practice and might confuse both users and tools. Also,
> it sounds like inferring the format won't be that hard.
>
> / Ulf
>
> On Sun, Oct 12, 2014 at 11:51 PM, Andrés Sicard-Ramírez
> <asr at eafit.edu.co <mailto:asr at eafit.edu.co>> wrote:
>
>
>     On 12 October 2014 06:28, Pepijn Kokke <pepijn.kokke at gmail.com
>     <mailto:pepijn.kokke at gmail.com>> wrote:
>
>         Try to infer the literate format from the file, making it
>         explicit with Agda command-line arguments if necessary.
>
>
>     +1
>
>
>     --
>     Andrés
>
>     _______________________________________________
>     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/