leanprover/doc-gen4

request: have the path to the current position unfolded by default

hrmacbeth opened this issue · 1 comments

In doc-gen3, if I follow a link to some declaration (e.g.
https://leanprover-community.github.io/mathlib_docs/algebra/group/units.html#units
) then the path to that declaration (algebra/group/units) is unfolded in the left navbar. Likewise if I search for that declaration (in that case, it keeps any previously-unfolded things open but also unfolds the thing being navigated to).

In doc-gen4, if I follow a link to some declaration (e.g.
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Units.html#Units
) then the path to that declaration (Mathlib/Algebra/Group/Units) is not unfolded; same if I search for the declaration.

I find the doc-gen3 behaviour more convenient; could it be copied over?

doc-gen3 generates pages with navbar included. It marks some html elements as as "open", so each page contains navbar unfolded at the correct place:

        {%- set is_open = 'open' if active_path.startswith(item.path+'/') else '' %}
        <details class="nav_sect" data-path="{{ item.path }}" {{is_open}}>
            <summary>{{item.name}}</summary>

(src)

doc-gen4 generates navbar is a separate html file which is included as an iframe, so it is not possible to "pre-render" unfolded.

The only solution I can think of is to use JavaScript to communicate with navbar after page load and to tell it which nodes to unfold.