Request: In library directory sidebar, preserve folded/unfolded state of each directory after a click
hrmacbeth opened this issue · 1 comments
hrmacbeth commented
In the mathlib3 docs, a directory which has been unfolded by clicking on it remains unfolded after you click on any other link. This is helpful, for example, if you wish to browse one by one through the files in some deeply-nested directory.
In docs4 it seems that after clicking any link, all directories get folded back again. Can this be changed?
hargoniX commented
This feature does exist in nav.js already but it stopped working at some point. I would not be surprised if this is because of the sidebar getting loaded via an iframe but I don't know to be honest.
If someone who actually knows what they are doing in the frontend wants to take a look feel free, I suspect the issue is rather nuanced.