Big header in web editor

Stream: lean4

[Jovan Gerbscheid]

I noticed that the web editor has suddenly gained a huge header taking up a large part of the screen. I understand that the web editor wants to be more closely integrated with the rest of the Lean website, but maybe there should be a full-screen mode that allows us to get the old behaviour back?

image.png

[Eric Wieser]

Or just making the header much more compact on this page

[Jovan Gerbscheid]

The issue is also that there are two headers, a big one and a small one. So I would suggest having the small one by default, with a button to also show the big header.

[Jovan Gerbscheid]

I now discovered that it is possible to get rid of the header by scrolling it away (but only if your browser is sufficiently zoomed in). But this scrolling is very inconvenient and unintuitive, because there are two separate scrolling mechanisms available at the same time: scrolling in the Lean file, and scrolling on the whole website. I think this double scrolling isn't new, but it's now more noticeable. Hopefully that can also be removed.

[Bryan Gin-ge Chen]

If you're OK with using an extension like Stylus to add a user style for live.lean-lang.org, you can remove the header with:

header {
    display: none;
}

[Asei Inoue]

Yes the header is huge…

[Bolton Bailey]

I noticed that the "use cases" link is broken. Is the source code for this website public and available for pull requests?

[Ashley Blacquiere]

Thanks everyone. We've noted the concerns and are reviewing to see if we can reduce the header real estate while still retaining navigation features that will support new users as they navigate the Lean site.

@Bolton Bailey - good catch on the use cases link. That's a typo. We'll make sure that gets fixed.

[Ashley Blacquiere]

FYI - As a solution to the concerns with the navigational header: We've added a Hide Navbar button to the hamburger menu above the InfoView. This setting persists across sessions, so you should need only activate it once (per browser, and assuming you don't empty your browser history).

image.png

[Jovan Gerbscheid]

Thanks for this! Although currently I don't see this extra button, nor the big header (i.e. it is back to the original form).

[Joscha Mennicken]

You only see the big header and corresponding button if you visit https://live.lean-lang.org/?from=lean, i.e. if you visit from https://lean-lang.org/.

[Jon Eugster]

Ashley Blacquiere said:

FYI - As a solution to the concerns with the navigational header: We've added a Hide Navbar button to the hamburger menu above the InfoView. This setting persists across sessions, so you should need only activate it once (per browser, and assuming you don't empty your browser history).

image.png

You could PR that button to the lean4web repo, if you'd like :)