Dots in qualified names are not included in links

[UlfNorell]

From wjedynak on December 07, 2011 22:54:50

What's the problem? Cut-and-pasted program examples are preferred over attachments (if reasonably short). Issue originally reported by Ramana Kumar. Dots in qualified names in HTML documents generated by agda --html are not included in the link text, so the links are broken into many parts, which is confusing.

I include a patch that fixes this issue in the simplest way. Generating docs for the std-lib seems to work, make test succeds. What version of Agda are you using? On what operating system (if relevant)? HEAD version.

Attachment: hyperlinks_dots.dpatch

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

[UlfNorell]

From nils.anders.danielsson on December 09, 2011 08:56:15

Thanks, but this patch is too hacky for my tastes. I don't want the HTML code to diverge too much from what is displayed by the Emacs mode.

Summary: Dots in qualified names are not included in links
Status: Accepted
Labels: Priority-Low Type-Enhancement

[UlfNorell]

From ramana.k...@gmail.com on December 09, 2011 09:04:40

I would say that the Emacs mode is equally broken in this respect. Is it more difficult to fix?

[UlfNorell]

From wjedynak on December 09, 2011 17:43:44

Thanks for reviewing. This time I tried to solve the problem in it's core. The fix from the attached patch applies both to emacs-mode and HTML generation (and any code that uses HighlightingInfo).

I may have missed something, but I think that the getModuleName helper in Generate.hs can call the (slightly modified) mod helper just once - this change allowed me to join the ranges in only one place (in the nameToFile function). I run the test suite and did some manual checks - it seems to work.

Attachment: dots_in_highlighting.dpatch

[UlfNorell]

From wjedynak on December 29, 2011 06:44:53

The patch from the previous comment would break the links inside mixfix operators (i.e. in 'if b then 1 else 0' the whole expression would link to if_thenelse). The attached patch doesn't have this flaw.

Attachment: dots_in_highlighting_fixed.dpatch