[Agda] Expanding literate Agda

[Sergey Kotikov]

Just W.A.D.
13 окт. 2014 г. 18:45 пользователь "Andreas Abel" <andreas.abel at ifi.lmu.de>
написал:

> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141013/ac0425c4/attachment.html