Plugin extension development: adding a widget to 'header' area of JupyterFrontEnd.IShell does not make the area visible

Hello again, Jason. Thanks very much for looking into this. I now understand the problem, and also have looked at the PR you made. I also looked at the original problem (https://github.com/jupyterlab/jupyterlab/issues/7279) and your explanations there, and I have posted some more questions there (trying to figure “where to post what” here!)