allow hyperlinks in "agda --html" generated files

[UlfNorell]

From escardo....@gmail.com on December 02, 2013 10:05:27

It would be nice to have a meta-command \url{...} to use in comments to generate links to documents within html agda files generated with "agda --html". It shouldn't be difficult to implement, I suppose.

Original issue: http://code.google.com/p/agda/issues/detail?id=986

[UlfNorell]

From nils.anders.danielsson on December 02, 2013 04:30:38

Sounds reasonable. I'm not sure if I like the \url{...} notation.

If we implement this, then I guess there should be some way to escape \url{...}, so that you can mention \url{...} in comments.

I can also imagine that people will want to use other kinds of annotations (consider things like JavaDoc and Haddock). Ideally the notation we choose for \url{...} should be forward-compatible with future extensions.

In order to avoid introducing a notation that might not fulfil the requirements above I suggest that we use a different approach: substrings that look like URLs can be turned into URLs automatically, if some flag is used (--turn-urls-into-links, say).

How does this sound?

Status: InfoNeeded
Labels: Type-Enhancement Priority-Medium Highlighting

[UlfNorell]

From andres.s...@gmail.com on December 02, 2013 04:43:51

The --turn-urls-into-links flag is a nice idea.

[UlfNorell]

From escardo....@gmail.com on December 02, 2013 04:50:07

It sounds good and easy: If I write http:// or ftp:// or https:// etc. then I get a link.

[UlfNorell]

From nils.anders.danielsson on December 02, 2013 05:33:51

Is anyone interested in implementing this? Pandoc provides a URI parser that seems reasonable, and could be used as inspiration: http://hackage.haskell.org/package/pandoc-1.12.1/docs/src/Text-Pandoc-Parsing.html#uri (Note that this parser is not exported from the Pandoc library, and Pandoc would have been a rather heavy dependency. Furthermore Pandoc is GPL-ed, so the code shouldn't simply be copied into Agda.)

Status: Accepted

[UlfNorell]

From nils.anders.danielsson on December 03, 2013 02:37:32

If we implement this, then I suggest that we make the links highlighted (and clickable) also in the Emacs mode, so that there is no need to inspect the generated HTML to find out if the links were detected correctly.

In this case we can either skip the --turn-urls-into-links flag, or add an option for it in the Emacs mode—I don't want to start my files with {-# OPTIONS --turn-urls-into-links #-}.