<p dir="ltr">Just W.A.D.</p>
<div class="gmail_quote">13 окт. 2014 г. 18:45 пользователь &quot;Andreas Abel&quot; &lt;<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt; написал:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Adding regular expressions to recognize more file extensions is easy for both the emacs-mode and Agda and the testsuite.<br>
<br>
If we decide on non-hierarchical file extensions, we could accept .*agda which would subsume .agda, .lagda, .bird-agda, .md-agda, .latex-agda, ...<br>
<br>
For hierarchical file extensions like .agda, .agda.tex, .<a href="http://agda.md" target="_blank">agda.md</a> it is only slightly more complicated.<br>
<br>
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<br>
<br>
$ cat icfp13-long.tex<br>
% The long version contains the appendix with figures<br>
% more proofs, and extra sections.<br>
<br>
\newcommand{\LONGVERSION}[1]{#<u></u>1}<br>
\newcommand{\SHORTVERSION}[1]{<u></u>}<br>
<br>
\input{icfp13}<br>
<br>
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.<br>
<br>
On 13.10.2014 15:35, Pepijn Kokke wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
If we use &quot;.lagda&quot; then currently agda-mode will be started and all Agda<br>
source is highlighted (and interactive, etc).<br>
<br>
If we use &quot;.lagda.tex&quot; then your editor will boot something like<br>
TeX-mode, where the TeX source is highlighted and the Agda source is<br>
(hopefully) untouched.<br>
<br>
As I see it, it&#39;s really a matter of preference.<br>
<br>
On 13 October 2014 14:08, Dominique Devriese<br>
&lt;<a href="mailto:dominique.devriese@gmail.com" target="_blank">dominique.devriese@gmail.com</a> &lt;mailto:<a href="mailto:dominique.devriese@gmail.com" target="_blank">dominique.devriese@<u></u>gmail.com</a>&gt;&gt; wrote:<br>
<br>
    All,<br>
<br>
    2014-10-13 13:55 GMT+02:00 João Paulo Pizani Flor<br>
    &lt;<a href="mailto:J.P.PizaniFlor@uu.nl" target="_blank">J.P.PizaniFlor@uu.nl</a> &lt;mailto:<a href="mailto:J.P.PizaniFlor@uu.nl" target="_blank">J.P.PizaniFlor@uu.nl</a>&gt;&gt;<u></u>:<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>
    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> &lt;<a href="http://lagda.md" target="_blank">http://lagda.md</a>&gt;&quot;.  The idea would be that editors (and<br>
    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><br>
    &lt;<a href="http://lagda.md" target="_blank">http://lagda.md</a>&gt;&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>
    ______________________________<u></u>_________________<br>
    Agda mailing list<br>
    <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;<br>
    <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br>
<br>
<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br>
</blockquote>
<br>
<br>
-- <br>
Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div>