Annotate pretty-printed output with full constant names

[gebner]

Motivation: we want to have links for all constants in the API documentation, even if they are behind notation. See companion PR leanprover-community/doc-gen#3.

This PR adds the option pp.links which, if set to true, annotates things like ℤ and + and the fst in p.fst with the corresponding constant names (i.e., int, has_add.add, and prod.fst). The markup syntax for this annotation is as follows:

<U+E000>prod.fst<U+E001>fst<U+E002>

The Unicode code points U+E000, U+E001, U+E002 are taken from the Private Use Area. Hopefully nobody uses them for anything else.

[gebner]

I also added a pp.generalized_field_notation that uses field notation for all function instead of just structure projections.

[Vtec234]

Do you think with the full knowledge of type information, we could link to the correct instance of a typeclass rather than the typeclass itself? E.g. the • in 1 • b = b could link to the inferred instance of has_scalar mytype rather than has_scalar.smul.

[gebner]

I would also like to see that. In practice I'm not sure there's an always an obvious choice for the instance declaration. E.g. in your example with •, the instance for has_scalar is mul_action.to_has_scalar, which is probably not what you want.

[cipher1024]

This looks good to me. I especially like what you did to pretty print projections. Ready to merge?

[gebner]

Yes, I think this can be merged. The pp.generalized_field_notation option is turned off by default though. Should we switch it on by default?

[robertylewis]

For doc gen reasons, could I request that this PR be included in a 3.5 release before we officially move mathlib over to 3.5?

[cipher1024]

Certainly. Sorry I completely lost sight of this PR. We can schedule 3.5.1 in the near future to make this PR available. Let's see if you have backward compatible PRs until then.

[robertylewis]

@cipher1024 In advance of the shift to 3.5c, could we merge this so it's part of the nightlies?