[Agda] URLs in comments

[Gabriel Scherer]

I myself use the following quick&dirty sed rewriting steps in my
blog-producing pipeline (for example
http://gallium.inria.fr/blog/bove-reloaded/ ).

  # replace markdown links
  sed -i 's/\[\(.*\)\](\(.*\))/<\/a><a style="color:blue;"
href="\2">\1<\/a><a class=\"Comment\">/' ./html/$@
  sed -i 's/\[\(http.*\)\]/<\/a><a style="color:blue;"
href="\1">[\1]<\/a><a class=\"Comment\">/' ./html/$@


On Wed, Apr 8, 2015 at 1:04 PM, gallais <guillaume.allais at ens-lyon.org>
wrote:

> Hi,
>
> A quick experiment with current agda + sed:
> https://gist.github.com/gallais/b29706fe7a0ee449b265
>
> The output (with no css file so it's ugly but whatever):
> https://rawgit.com/gallais/d167209cd1501f017e5b/raw/Url.html
>
> On 07/04/15 20:32, N. Raghavendra wrote:
>
>> Is there a way to write URLs in comments in Agda files so that the URLs
>> become clickable in HTML files generated from the source?  Things like
>> writing <a href="http://www.example.net/">Example</a> don't work because
>> the entire text is enclosed in a pre element in the generated HTML.
>>
>> Cheers,
>> Raghu.
>>
>>
> _______________________________________________
> 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/20150408/643c1ebd/attachment.html