PatrickMassot/leanblueprint

Triangle before proof not correctly shown if `showmore` is enabled

Opened this issue · 1 comments

TL;DR

In project PFR and alike, the triangle before a proof shows ▼/▶ for proof collapsing/expansion, which is the opposite of how one expects them, where ▼ should indicate proof expansion. Also, it's the opposite of project LTE.

Reported by @kbuzzard .

Details

What's expected

In LTE ( code, rendered ), showmore is NOT enabled, the triangle before proof is shown as ▼, and the proof is expanded by default, so ▼ indicates proof expansion correctly.

Afterward, clicking on the triangle works as expected, the triangle toggles between ▼ and ▶ , indicating the proof is expanded and collapsed, respectively.

image

What went wrong

In PFR ( code, rendered ), showmore is enabled, besides the eye +/- icons appear below and can control the level of details to show, by default, it collapses proofs, but the triangle before proof is still shown as ▼, so ▼ is not correctly corresponding to the proof collapsing status but the opposite.

image

Afterward, clicking on the triangle will never works as expected, it's always the opposite, unless one click on the eye +/- icon odd times, then this would be reversed and fixed.

Cause

The clicking of the triangle and the show more handles the triangle states separately, causing the confliction, plus they have different defaults.

Workaround

Don't enable showmore until this issue is fixed: In web.tex

Change the line like

\usepackage[showmore, dep_graph, project=../../]{blueprint}

to

\usepackage[dep_graph, project=../../]{blueprint}

Thanks for the report. I noticed something was weird but never bothered because this convention always seemed unclear to me. It should be fixed by d336038.