Zulip Chat Archive

Stream: general

Topic: highlighted formatting in docs

Rob Lewis (Sep 24 2020 at 11:26):

Poll:

:framed_picture: for the frame color (https://github.com/leanprover-community/doc-gen/pull/73)
:rainbow: for Gabriel's original gradient (https://github.com/leanprover-community/doc-gen/pull/59#issue-475923398)
:peace: for the groovy tie dye option (https://github.com/leanprover-community/doc-gen/pull/59#issuecomment-683736233)

Eric Wieser (Sep 24 2020 at 11:41):

A possible suggestion - can we highlight prop-valued expressions in a different color to other expressions?

Eric Wieser (Sep 24 2020 at 12:03):

In fact, it might be neat if the type of the hovered expression was shown in title text

Rob Lewis (Sep 24 2020 at 12:18):

Types of subexpressions (even just prop/non-prop info) takes a lot more processing when we generate the data. Storing the type of every subexpression that appears in the type of every decl of mathlib is a crazy amount of data.

Rob Lewis (Sep 24 2020 at 12:20):

I suspect coloring prop/non-prop arguments differently would be more visually confusing than enlightening, and since it's not trivial to even export that data, I don't think it's worth trying right now.

Rob Lewis (Sep 24 2020 at 12:22):

But I do like the "frame color without hue shift" you suggested in the PR: image.png

Rob Lewis (Sep 24 2020 at 12:22):

The distinction between shades is a little hard to see in the static screenshot, but trying it live, there's a nice subtle effect.

Rob Lewis (Sep 24 2020 at 12:25):

On showing types on hover: what IS possible, without changing the data export at all, is to show the types of constants on hover. Basically, anything that gets linkified now could have a tooltip showing its type. Not its type in the current application, but the type of the declaration.

Rob Lewis (Sep 24 2020 at 12:26):

Problem is, this is potentially a lot of information, it would lead to some very big tooltips.

Gabriel Ebner (Sep 24 2020 at 12:45):

Frame color w/o hue shift is definitely better than the yellow-green gradient.

Rob Lewis (Sep 24 2020 at 13:12):

Gabriel Ebner said:

Frame color w/o hue shift is definitely better than the yellow-green gradient.

Agreed, I thought the shade differences would be too subtle, but in practice it works.

Eric Wieser (Sep 24 2020 at 13:16):

I think a border-radius: 5px like in the rainbox scheme helped a little with spotting boundaries

Rob Lewis (Sep 24 2020 at 13:21):

I didn't even notice that -- very subtle, but it doesn't hurt. Also I changed my mind, you were right with 5% steps.

Rob Lewis (Sep 24 2020 at 13:22):

image.png

Eric Wieser (Sep 24 2020 at 13:31):

Or perhaps with borders:

.theorem .fn:hover {
    background-color: hsla(115, 62%, calc(100% - 5%*var(--fn)));
    box-shadow: 0 0 0 1px hsla(115, 62%, calc(100% - 5%*(var(--fn) + 1)));
    border-radius: 5px;
}

etc

image.png

Rob Lewis (Sep 24 2020 at 13:39):

Ooh, the borders are a big improvement.

Rob Lewis (Sep 24 2020 at 13:43):

This is going live now, check the docs in a few!

Rob Lewis (Sep 24 2020 at 13:58):

https://leanprover-community.github.io/mathlib_docs/geometry/euclidean/circumcenter.html#euclidean_geometry.exists_unique_dist_eq_of_insert

Patrick Massot (Sep 24 2020 at 14:01):

Beautiful!

Patrick Massot (Sep 24 2020 at 14:01):

I prefer blue to green. What about switching the color code between def and lemma?

Last updated: Dec 20 2023 at 11:08 UTC