Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Options for padding around the tab bar - Final #3685

Closed
wants to merge 11 commits into from
Closed

Options for padding around the tab bar - Final #3685

wants to merge 11 commits into from

Conversation

jsphnecclia
Copy link

See 3436 and 3684

Adds options for padding/margin around the tab bar.

@salmankhilji
Copy link

I am wanting this feature as well; however, it has a few issues. I cloned your repo and tested as follows:

  1. With the tab bar on the top edge, it leaves a margin at the top of the OS window, the tabs can not be clicked on with the mouse. Please recall that its easier to click the edge of the screen then it is to overshoot and have to bring the pointer down by the tab_bar_margin_height value to click a tab. I suggest extending the mouse clickable area to the edge of the screen above or below the tab bar.

  2. Open two tabs within a new kitty window that starts as non-maximized, non-full screen. Mine was 128cx32c. Then CTRL+SHIFT+F11 to go to full screen and then back to normal size window. You will now see that the taba can not be clicked on, and kitty is in bad state. Here is a stack trace.

$ kitty/launcher/kitty 
Traceback (most recent call last):
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/boss.py", line 680, in dispatch_possible_special_key
    return self.dispatch_action(key_action)
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/boss.py", line 751, in dispatch_action
    passthrough = f(*key_action.args)
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/boss.py", line 1371, in launch
    launch(self, opts, args_)
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/launch.py", line 360, in launch
    tab = tab_for_window(boss, opts, target_tab)
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/launch.py", line 200, in tab_for_window
    tab: Optional[Tab] = tm.new_tab(empty_tab=True, location=opts.location)
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 734, in new_tab
    self._add_tab(Tab(self, no_initial_window=True) if empty_tab else Tab(self, special_window=special_window, cwd_from=cwd_from))
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 589, in _add_tab
    self.tabbar_visibility_changed()
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 605, in tabbar_visibility_changed
    self.resize(only_tabs=True)
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 625, in resize
    tab.relayout()
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 199, in relayout
    self.relayout_borders()
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 206, in relayout_borders
    self.borders(
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/borders.py", line 85, in __call__
    left, top, right, bottom = br
TypeError: cannot unpack non-iterable int object
Traceback (most recent call last):
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/boss.py", line 537, in on_window_resize
    tm.resize()
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 625, in resize
    tab.relayout()
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 199, in relayout
    self.relayout_borders()
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 206, in relayout_borders
    self.borders(
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/borders.py", line 85, in __call__
    left, top, right, bottom = br
TypeError: cannot unpack non-iterable int object
Traceback (most recent call last):
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/boss.py", line 529, in activate_tab_at
    tm.activate_tab_at(x, is_double)
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 819, in activate_tab_at
    self.set_active_tab_idx(i)
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 631, in set_active_tab_idx
    tab.relayout_borders()
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 206, in relayout_borders
    self.borders(
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/borders.py", line 85, in __call__
    left, top, right, bottom = br
TypeError: cannot unpack non-iterable int object
  1. Open a new kitty window that starts as non-maximized, non-full screen. Mine was 128cx32c. Go to full screen. Open two tabs. Restore from full screen. You will now see the fonts all garbled up. See screenshot and stack trace below:
$ kitty/launcher/kitty 
Traceback (most recent call last):
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/boss.py", line 537, in on_window_resize
    tm.resize()
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 625, in resize
    tab.relayout()
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 199, in relayout
    self.relayout_borders()
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/tabs.py", line 206, in relayout_borders
    self.borders(
  File "/home/precor/Scratch/kitty/kitty/launcher/../../kitty/borders.py", line 85, in __call__
    left, top, right, bottom = br
TypeError: cannot unpack non-iterable int object

before:

before

after:

after

@jsphnecclia
Copy link
Author

jsphnecclia commented Jun 3, 2021

  1. I'll look into expanding the clickable area for the tab.
  2. I (on macOS) can not replicate your second bug. That stack trace is strange -- I did not edit tabs.py, borders.py, boss.py, etc. What happens if you replace the tab_bar.py in my repo with the one in the main repo? This should make the font/text more garbled but maybe the stack errors may go away?

If you have the skill, could you try to fix these issues yourself? I'll be working on them simultaneously, but I can't work well on a bug I can't replicate

EDIT: I looked into expanding the clickable area, and it would be nontrivial to implement. Currently the margin height is implemented by pushing the tab bar down or raising it up, depending on whether the tab bar is on the top or bottom edge. On the bottom the extra height is below the tab bar, part of the tab bar, while on the top the extra height is above the tab bar, that is, not part of the tab bar, but before it. I'll still keep looking for a way to get around this, but I spent a lot of time in this part of the code and don't know of another way to do it. Plus, having the clicking functionality relegated correctly to the tab bar text isn't apparently a bad thing. If I had more knowledge of the tab bar itself, that is, knew how to add padding in the tab bar before the tab bar text itself, I may be able to do it (expand the clickable area)

@jsphnecclia
Copy link
Author

Pretty sure I just fixed your fullscreen issue, will you try it and let me know?

At any rate, having another set of eyes is always good for these things, maybe you can figure out about extending the clickable area?

@salmankhilji
Copy link

I have confirmed your changes have fixed the full screen issue.

Unfortunately, I don't have time to dig into the source code myself to look into the extending the clickable area.

One thing that is odd though is that the clickable area does indeed extend to the bottom edge of the OS window when the tab bar is at the bottom. Its only when the tab bar is at the top that the clickable area does not extend to the top edge of the OS window. Should be consistent IMHO.

How difficult would it be to not just have padding between the tab bar and the edge of the OS window but also on the other side? i.e., have padding on both sides of tab bar?

In my setup, I'd keep the tab bar at the top with the top padding set to 0 and use just the bottom padding. As you can see, my PS1 is too close to the tab bar in the screenshot below:

Screenshot from 2021-06-03 18-40-06

I want it spaced out little. Though what I want can be somewhat achieved using window_padding_width, the issue is that doing so affects all windows when I split them, not just windows along the top edge of the screen where the tab bar is.

@jsphnecclia
Copy link
Author

For the click area, as I said above:

Currently the margin height is implemented by pushing the tab bar down or raising it up, depending on whether the tab bar is on the top or bottom edge. On the bottom the extra height is below the tab bar, part of the tab bar, while on the top the extra height is above the tab bar, that is, not part of the tab bar, but before it.

Basically, I didn't edit the clickable area, I don't know how to. It working correctly when on the bottom edge is just a side effect.

If I had more knowledge of the tab bar itself, that is, knew how to add padding in the tab bar before the tab bar text itself, I may be able to do it (expand the clickable area)

As for the padding on both sides of the bar, I should be able to implement that and am working on it right now

Some help from a maintainer may give the needed push in the right direction for the click area, but as for now (once I get the padding on both sides feature in) I'll go ahead and call it complete

@kovidgoyal
Copy link
Owner

Note that for clickable area, relevant code is in mouse.c

@jsphnecclia
Copy link
Author

jsphnecclia commented Jun 4, 2021

Is there an easy way to set up an option like the window_padding_width that takes in multiple values at the same time? I think it would be cleaner to do like tab_bar_margin_height 19.0 22.0 or something rather than

tab_bar_margin_height_outer 19.0
tab_bar_margin_height_inner 22.0

I have looked in mouse.c but I couldnt seem to find something relevant to what I need, and nothing about making clicks outside of the tab bar (above/"before" it). The most relevant piece I saw is window_for_event, which points back to os_window_regions in state.c -- but no way to add the clickable padding between the os window top and the start of the content for the tab_bar. My looking into mouse.c has circled back to os_window_regions, the function I was editing in the first place. This suggests that I've been editing the clickable areas the whole time -- still I don't know how to add the clickable padding to before/above the text?

Almost done with the inner and outer padding

@kovidgoyal
Copy link
Owner

kovidgoyal commented Jun 4, 2021 via email

@jsphnecclia
Copy link
Author

Could you take a look at my os_window_regions code? I feel like I'm doing what youre suggesting (like when I set the padding through tab_bar->top = pt_to_px(OPT(tab_bar_margin_height), os_window->id)) but I get an unclickable area on top, as if it were pushed down instead of added padding to. Yet below the tab bar, between the bar and the prompt, tabs are clickable

@jsphnecclia
Copy link
Author

@salmankhilji see if the latest merge works how you wanted. Use the settings tab_bar_margin_inner and tab_bar_margin_outer

@kovidgoyal kovidgoyal closed this in 091fec0 Jun 5, 2021
@kovidgoyal
Copy link
Owner

I just implemented it myself, less work than reviewing your code, but thanks for the implementation, it helped guide me. Note I dropped the retain option, as I dont much see the point of it.

@jsphnecclia
Copy link
Author

The retain option is pivotal for me. Without it there's no way to set the padding of the top of the window to the prompt (when there are not enough tabs to activate the tab bar) that doesn't have unexpected side effects when the tab bar activates.

(Really the pivotal option would be 'min_tab_margin_height', 'retain_tab_bar_margin_height' was a work around to get what I think would be the most common use of the 'min_tab_margin_height' option, that is, say if you have a tab_bar_margin_height.outer of 19.0, the min_tab_margin_height would take the value of 19.0. A more customizable min_tab_margin_height would be better, though.)

'min_tab_margin_height' would be an option for padding between the top of the window and the padding specified by window_padding_width/window_margin_width. It 'takes the place' of the tab bar when the tab bar is not hidden, but also not yet activated by the requisite amount of tabs.

Screen Shot 2021-06-05 at 11 34 51 AM

This is ok: but if you want to add padding between the top of the screen and the prompt you would use window_padding_width. However, window_padding_width means different things in different places. You come across this difference often when opt.tab_bar_hidden is false and min_tab is set. When there is no tab bar it is between the top of the screen and the prompt -- but when the tab bar is present, window_padding_width is between the tab_bar and the prompt, as opposed to the top of the screen and the tab bar, which is what you might expect. Instead that area is defined by tab_bar_margin_height.outer. If you try to add padding with the tab bar gone, you end up with something like this:

Screen Shot 2021-06-05 at 12 41 40 PM

Sure there's padding without the tab bar, but this padding translates to a messed up, bloated tab bar when it does activate.

Screen Shot 2021-06-05 at 11 52 29 AM

This is better: It is usable/beautiful with both one/no tabs and with tabs amounting to above min_tab. The top of the window is coherent. It's pretty. It's functional. It is what I set out working on this feature to achieve. It's definitely a feature worth adding in to the app, and, After spending so much time on this feature, It would really suck to have to patch it in manually every time I update the app. I definitely think that I could not be the only user who would use such a feature.

(Also where the meaning of retain_tab_bar_margin_height might be confusing, min_tab_bar_height is more descriptive/shows the point of the feature better. Im no longer advocating retain_tab_bar_margin_height as I think you solved the issue I had that limited me to a bool value rather than a point float, but I am certainly advocating for min_tab_bar_height)

@kovidgoyal
Copy link
Owner

I dont follow, simply set tab_bar_min_tabs to 1 that way the tab bar will always be present and you can use the new options to control the padding. Nor do i understand why you would want padding between the top of the contents and the top of the OS Window, but not want it between the top of the contents and the bottom of the tab bar when it is visible.

@kovidgoyal
Copy link
Owner

In the case where you want the tab bar to be invisible for one tab set the inner tab bar margin to 0 and use window padding with an outer tab mar margin. That way you get the same gap between the top of the window and either the shell or the tab bar regardless of whether it is visible.

@jsphnecclia
Copy link
Author

It doesn't make sense to have a tab bar of one (especially when decluttering is a goal), and sometimes min_tabs may be set for higher than one or two in normal use anyway.

It's not that I want padding between the top of the contents and the OS window and not the top of the contents and the bottom of the tab bar, it's that I want different padding between the two. Like in my second set of images above - I want that 27.0 (27.0 window_padding_width) point padding on the left, but not the 36.0 (19.0 tab_bar_margin_height_outer + 27.0 window_padding_width) padding in the tab bar on the right. Instead (in the last set of images) I want the 27.0 (8.0 window_padding_width padding + 19.0 min_tab_margin_width) on the left and 27.0 (19.0 tab_bar_margin_height.outer + 8.0 window_padding_width) on the right.

I don't think I was able to get your 'invisible tab bar' effect to work, and I don't think thats what I'm thinking of anyway:
Screen Shot 2021-06-06 at 11 45 54 AM

Here the tab bar is also bloated and ugly. Again the margin on the left has a different semantic meaning than the difference on the right. Again, there's no way to set the padding of the top of the window to the prompt (when there are not enough tabs to activate the tab bar) that doesn't have unexpected side effects when the tab bar activates. It is a subtle difference but it carries a lot of weight.

It makes sense to add the min_tab_margin_height to our update containing a set of different tools for managing the tab bar.
Where the one setting of the padding looks right, in another place the padding looks wrong. This points to the fact that the one setting should actually be separated into two settings. This is a feature that is trivial to add, and it makes our set of tab bar margin tools complete. I will be adding this feature for myself, but that's no fun for updates and is a really sucky way to end the past few months where I've been working on this feature (I sunk a lot of time working on this), when I'm sure that others would find a use for it as well. I hope you will reconsider and add the feature, if not by the points I made then by the strength of belief in which I made them.

@kovidgoyal
Copy link
Owner

kovidgoyal commented Jun 6, 2021 via email

@jsphnecclia
Copy link
Author

You are saying you want more space between content and OS window margin
and less space between content and tab bar. My question is WHY?

You are just arbitrarily deciding one looks ugly and one doesnt.

I don't think arbitrary is the right word. It's an aesthetic difference that is hard to explain

You basically want this because it looks nice to you
to have a smaller gap between the content and the tab bar than between the
content and the outer window margin. I really dont see why that makes
sense.

Basically, yes, but I don't think I'm the only one who would think so/prefer the option.

I have yet to be convinced that setting the tab bar outer margin and
window padding to the same value and tab bar inner margin to zero looks
ugly.

With aesthetics it is often hard to describe why something looks off or ugly, like it was hard to explain why a tab bar with a little padding from the top was better than one with no padding. I mentioned things being ugly here because I expected you to see what I see without needing the explanation, which falls short of and is less powerful than experience. I will try to explain but it comes down to a gut feeling:

  1. First of all, and probably most importantly, I want more space between content and OS window margin and less space between content and tab bar because the tab bar is in a class of semi-content. It is neither fully noncontent, nor fully content. As opposed to empty padding on the edge of the window, a tab bar is content and thus shouldn't be grouped too separately from content. Yet, it makes sense to group tab bar and content together because a tab bar is much like content. But some margin is preferable, because the tab bar is also not content, and operates differently from the content below it.
  2. Second, with min_tab_margin_height, you can make the padding between the edge of the window and any content at all (here including the tab bar) consistent, whether min_tab has activated the tab bar or not. (The mouse-draggable window margin/padding #3683 may solve this, but it may not)
  3. Third, It makes the 'header' of the window too large. Say your values are 27.0 for window_margin_width.top, 27.0 for tab_bar_margin_height.outer. That's the 'invisible tab bar' method you mentioned. That's 54.0 total for the tab bar + margin. That is way too high! with min_tab_margin_height, a similar set up would be 27.0 point both with and without the tab bar! It is definitely preferable to have clean tabs without the extra 'wasted' space being too top heavy.
  4. Less importantly, I feel like the tab bar should be slim vertically, how it is when there is no padding on either side. When the space between the edge of the window and the tab bar is large, this does not matter as much because it appears like empty space before the tab bar, as opposed to that space being part of the tab bar. However, when the space between the content and the tab bar is large, it appears like the tab is large, instead of being empty space. I think that's one of the reasons the 'invisible tab bar' method appears ugly/bloated to me.

I could list more but I hope now you see that my thinking is not arbitrary.

I'd like to mention again here what I said above: There's no way to set the padding of the top of the window to the prompt (when there are not enough tabs to activate the tab bar) that doesn't have unexpected side effects when the tab bar activates.

Sorry it doesn't make sense to me. And I am yet to hear from anyone else
that says they want this feature.

I meant that while no one would think to ask for this feature, if it were added people would stumble upon it when configuring their tab bar and be like "I didn't know I needed this" and use it.

And no, whatever time you spent on
this feature was for YOUR benefit, not mine.
I spent a whole bunch of
time guiding you and helping you, to the extent of actually implementing
it for you, for something that is utterly useless to me. It doesn't
obligate me to add what I feel is pointless bloat.

I am not saying the time I sunk was for your benefit, that's not what I meant at all. It most certainly was for my benefit, I learned a lot, I figured out a lot. I am very thankful for your help over and over again with the whole project - I was almost done with my implementation when you finished it for me. It meant a lot to me. I want to share what I worked on with everyone else.

I'm unclear what you're referring to as pointless bloat -- Is that just min_tab_margin_height or the whole tab bar padding feature? I'm sorry you feel that way :/

I think you are confusing the semantics of window_padding_with. window
here refers to kitty windows, more than one of which can be in a single
tab. They are not about defining the spacing between the border of the
OS Window and the content in it.

What you really want is to be able to define padding for OS Window.
This will let you specify the space between the borders of the OS Window
and any content inside it. And then you can independently specify the
spacing between the tab bar and content below it using the setting I
just added.

And this makes sense to me. I am willing to merge a patch that adds a
new setting: os_window_padding_width modeled on window_padding_width.

With this setting you will get the effect you think looks nice by
setting os_window_padding to X for the top edge and tab bar inner margin
to Y. X wil be the spacing between the content and the os window border
when the tab bar is hidden and Y will be the spacing between the content
and the tab bar when the tab bar is visible.

And this will make it possible to implement #3683 as well

I am not sure if that's what I'm going for or not, plus that's the start of a whole new project.
And it looks like someone is already working on the feature anyway (probably much faster and more fruitfully than I could) in a different way. (I'll keep my eye on it)

Anyway - you can see now that my thinking is not arbitrary, but has a lot of reason behind it, and I hope you will rethink the inclusion of min_tab_margin_height. With the inclusion of min_tab_margin_height, there would be a sensible way to add padding however large at all states of the process:

  • with tab_bar set to hidden
  • with tab_bar set to min_tab without the tab_bar being activated
  • with tab_bar set to min_tab with the tab_bar being activated

I mainly wanted to address this point of yours:

You are saying you want more space between content and OS window margin
and less space between content and tab bar. My question is WHY?

You are just arbitrarily deciding one looks ugly and one doesnt.

I gave my why and explained my decision process. Now I'll leave it to you.

I understand if you don't see it this way, it's your project. and I don't mean to 'fan the flames' of this discussion with this long post, but I just had to try to offer an in-depth explanation of the way I see it, in the hopes that you might see it that way too. If not, oh well. Sincerely, thank you, for making this program and maintaining it and everything, and especially for the time you spent helping me out. Cheers for tab bar margin!

@kovidgoyal
Copy link
Owner

kovidgoyal commented Jun 7, 2021 via email

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants