Reduce space used in fixed top regions so smartphones can show more statements

[david-a-wheeler]

The top regions, namely, the "Loaded: ..." area, the "Settings/Editor" tab selection bar, and the Editor icon bar have too much space (especially when the Editor icon bar overflows into multiple lines). Also, on narrow screens the icon bar overflows into multiple lines.

This is a big problem on smartphones because their built-in displays have so few pixels. It still works, but if these fixed regions took less space, there'd be a lot more room to play with :-).

This isn't as big a deal on laptops, but even there, most displays are wide but have limited vertical space.

At the least, tweaking the CSS to reduce the vertical padding would probably give at least another line back.

Even more interesting would be tweaking the icon bar so that if there isn't enough room some less-used icons would flow into an overflow menu (the "3 dots" icon). On smartphones in particular that would be really nice - it works without, but that would definitely improve things.

[david-a-wheeler]

Also: if the screen has a narrow width less horizontal padding between the icons on the icon bar would be great. The icon bar should always be 1 line, with overflow icons flowing into a "..." icon.

[david-a-wheeler]

Here's a picture showing what I mean:

A lot of space is taken by a region that isn't movable on a smartphone, leaving less room for manipulating the proof statements themselves.

See also #70.

[expln]

As I replied in #70 I plan to hide the heading completely. I will check what I can do with other "space consumers".

[expln]

@david-a-wheeler

I made few changes to reduce the fixed top area:

• it is possible to hide the context header completely:

1. In the settings select "Hide context header" checkbox and "apply changes" button.
2. With that setup, the context header will disappear instead of being collapsed.
3. In order to reveal it again, you don't have to go to the settings.
   In the editor and in the proof explorer (PE) main page use the "Show context" menu item of the "hamburger" menu.
   In a proof explorer tab for an assertion there is no such possibility at the moment. Just switch to the editor or the main page of the PE and use the "Show context".
4. If the context header was shown only to check current scope, and you are not going to change it, you may click the top grey area and this will hide the context header.

• height of tabs is reduced.

• while working in the editor, it is possible to hide the tabs completely:

1. Use the "Hide tabs" menu item of the "hamburger" menu in the editor to hide the tabs.
2. Without tabs, you obviously cannot switch to other tabs. To show them again, use the "Show tabs" menu item of the "hamburger" menu in the editor.

• The problem with the toolbar (Editor icon bar) overflowing into multiple lines is not resolved. I spent some time to implement a solution when the toolbar becomes scrollable. But this was difficult to implement correctly (and not to make the solution even more bad than the current situation). Implementing the toolbar flows into an overflow menu "..." is more difficult and time-consuming. So I implemented another solution: you may make buttons smaller. They will still overflow into multiple lines, but overall the toolbar will take less space. This solution is also good because you have instantaneous access to all the buttons without the need to click some intermediate buttons or doing a scroll action. To make buttons smaller use the "View options" menu item of the "hamburger" menu in the editor, then select "Small buttons" in the opened dialog.

I guess you've already noticed these changes on the dev, and probably you didn't need such detailed explanations, but I wrote it for documenting purposes too (it will be easier for me to copy-paste parts of the text to the guide when I will have to update it).

I saw your PR for tweaking the text on the context header. I want to test it locally, and then I will reply in the PR.

[david-a-wheeler]

@david-a-wheeler

I made few changes to reduce the fixed top area:
* it is possible to hide the context header completely: ...

Yes, I noticed and appreciated all those improvements. I've been using them. The smaller tool buttons really make a big difference. The marching off the side with dynamic tabs is something that can wait for some future release; it's currently odd but easily worked with. I'd prioritize undo and unification over the marching tabs frankly.

It's nice to be able to completely eliminate the context tab, but it's also nice if the contect tab can seen. If the context text is shortened it's often fine, and my tweak loses no information. I'd prefer both shorter context text and the ability to suppress it.

I tried to capture "update guide on version 11 release" here:
metamath/lamp-guide#78

[expln]

It's nice to be able to completely eliminate the context tab, but it's also nice if the contect tab can seen. If the context text is shortened it's often fine, and my tweak loses no information. I'd prefer both shorter context text and the ability to suppress it.

At the moment I am not ready to shorten the header. Please see my response here #70 (comment)

If you really want to see a shortened header on smartphones I can propose creating an optional "short format" for header on smartphones which will be switched on/off in the settings. This "short format" may be even more short than what we get by just removing the "stopped" word from the existing format - we may use special symbols like round and squared brackets or something like that with meaning "included" and "excluded", to make the format really short. Please let me know what you think about this.

[david-a-wheeler]

"Shortened header" sounds good. That's quite consistent with having other options to reduce display space.

[expln]

I created a separate issue for "Shortened header" #119

I've just recently released v11. Please, confirm that this issue may be closed.

[david-a-wheeler]

CONGRATS on v11 release!!

The other changes help, and we can continue discussions on #119. I'll close this one.

[expln]

Thank you!