<div dir="ltr">If we use &quot;.lagda&quot; then currently agda-mode will be started and all Agda source is highlighted (and interactive, etc).<div><br></div><div>If we use &quot;.lagda.tex&quot; then your editor will boot something like TeX-mode, where the TeX source is highlighted and the Agda source is (hopefully) untouched.</div><div><br></div><div>As I see it, it&#39;s really a matter of preference.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On 13 October 2014 14:08, Dominique Devriese <span dir="ltr">&lt;<a href="mailto:dominique.devriese@gmail.com" target="_blank">dominique.devriese@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">All,<br>
<span class=""><br>
2014-10-13 13:55 GMT+02:00 João Paulo Pizani Flor &lt;<a href="mailto:J.P.PizaniFlor@uu.nl">J.P.PizaniFlor@uu.nl</a>&gt;:<br>
&gt; But I also think &quot;double extensions&quot; should be avoided, and one reason for<br>
&gt; avoiding them is that external tools might get (very) confused.<br>
&gt;<br>
&gt; Text editor, standalone highlighters, plugins for CMS&#39;s, all of these tools<br>
&gt; that now assume that &quot;.{,l}agda = Agda&quot; and &quot;.tex = TeX&quot; will have to change<br>
&gt; their assumptions.<br>
&gt;<br>
&gt; It would be interesting, for example, that Literate Agda in LaTeX style is<br>
&gt; shown in a text editor with Agda highlighting. If &quot;double extensions&quot; are<br>
&gt; adopted, then a text editor might see the &quot;.tex&quot; extension, ignore what<br>
&gt; comes before, and show only TeX highlighting (ignoring the possibility of<br>
&gt; highlighting the Agda fragments).<br>
&gt; Even though we control the &quot;official&quot; Emacs mode, forcing these extension<br>
&gt; &lt;-&gt; filetype associations upstream to other tools would be too much effort.<br>
<br>
</span>I want to argue the opposite point :).  If we make sure, for example,<br>
that literate Agda files with markdown support are still valid as<br>
normal markdown files, similar to how lagda files are valid latex<br>
files, then it makes sense to use extensions like &quot;*.lagda.tex&quot; or<br>
&quot;*.<a href="http://lagda.md" target="_blank">lagda.md</a>&quot;.  The idea would be that editors (and other tools) that<br>
don&#39;t know Agda will automatically treat these as &quot;*.tex&quot; or &quot;*.md&quot;<br>
(i.e. use the standard highlighters/editing support for those<br>
formats).  This would be a good thing because highlighting<br>
&quot;*.lagda.tex&quot; as &quot;*.tex&quot; is better than highlighting &quot;*.lagda&quot; as<br>
plaintext. The Agda-mode (which we control) and potentially other<br>
editors which are aware of Agda (are there any so far?) and the<br>
&quot;lagda.*&quot; idea could then treat them as &quot;*.lagda.tex&quot; or &quot;*.<a href="http://lagda.md" target="_blank">lagda.md</a>&quot;.<br>
<br>
&gt; Sorry for bikesheding,<br>
<br>
Same here :).<br>
<br>
Regards,<br>
Dominique<br>
<br>
P.S.: Kudos to the people doing the actual work ;)<br>
<div class="HOEnZb"><div class="h5">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>