Current DocGen hyperlink system is as following:

(Lean.)Expr
  -(DocGen4.Process.)prettyPrintTerm→
(Lean.Widget.)CodeWithInfos
  -(DocGen4.Output.)docInfoToHtml→
(DocGen4.)Html

CodeWithInfos is text sent to the infoview to display terms with additional datas when hovered.

For example, let's see what CodeWithInfos sent to the infoview when it display List.insert 0 [1, 2].

.tag
  { expr := (q(List.insert 0 [1, 2]) : Expr), subexprPos := Pos.fromString! "/", .. }
  (.append
    #[.text "List.insert ",
      .tag
        { expr := (q(0) : Expr), subexprPos := Pos.fromString! "/0/1", .. }
        (.text "0"),
      .text " ",
      .tag
        { expr := (q([1, 2]) : Expr), subexprPos := Pos.fromString! "/1", .. }
        (.append
          #[.text "[",
            .tag
              { expr := (q(1) : Expr), subexprPos := Pos.fromString! "/1/0/1", .. }
              (.text "1"),
            .text ", ",
            .tag
              { expr := (q(2) : Expr), subexprPos := Pos.fromString! "/1/1/0/1", .. }
              (.text "2"),
            .text "]"])])

prettyPrintTerm does the same process when display terms on the infoview, but DocGen runs prettyPrintTerm with set_option pp.tagAppFns true; this option makes constant application tagged with its constant. So, in the last example, #[.text "List.insert", ..] becomes #[L.tag { info := ⟨{ info := { expr := (q(@List.insert) : Expr), .. }, .. }⟩, .. } (.text "List.insert"), .text " ", ..].

Then, docInfoToHtml hyperlinks text tagged with constants.

However, current DocGen doesn't hyperlink field notations; .Nodup in [0, 1, 2].Nodup isn't hyperlinked to List.Nodup, this is because pp.tagAppFns doesn't tag field notations.

This problem comes from the limitation of pp.tagAppFns, so the solution is refactoring pp.tagAppFns to tag field notations, or refactoring docInfoToHtml to hyperlink terms without relying on pp.tagAppFns, so I chose the latter solution.

The new docInfoToHtml hyperlinks CodeWithInfos without constant tags, if decInfoToHtml find a constant application tag, then it checks whether all tags of explicit arguments of the tag appear in direct children. If so, it hyperlinks non-tagged text in direct children.

It hyperlinks more notations such as field notations.

As a special case, when fun x => t(x) appears as a explicit argument, docInfoToHtml allows to appear t(x) instead of fun x => t(x), to hyperlink binder notations like { s : String // 0 < s.length }.

⚠ Improvement points

Sometimes, parenthesis maybe hyperlinked. This is because docInfoToHtml hyperlinks text according to info.

resolves #91, resolves #224