mirrors/kitty
1
0
Fork 0
mirror of https://github.com/kovidgoyal/kitty synced 2026-07-16 13:34:48 +02:00
Code Issues Packages Projects Releases Wiki Activity

Fix border/margin/padding sizes not being recalculated on DPI change

Browse Source 
Fixes #2346
Fixes #2347
This commit is contained in:
Kovid Goyal
2020-02-09 08:31:09 +05:30
parent 53f7eebc4d
commit c1abb7038d
5 changed files with 36 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
kitty/borders.py
View File

@@ -48,11 +48,9 @@ def load_borders_program():
class Borders:
def __init__(self, os_window_id, tab_id, opts, border_width, padding_width):
def __init__(self, os_window_id, tab_id, opts):
self.os_window_id = os_window_id
self.tab_id = tab_id
self.border_width = border_width
self.padding_width = padding_width
self.draw_active_borders = opts.active_border_color is not None
def __call__(
@@ -61,6 +59,8 @@ class Borders:
active_window,
current_layout,
extra_blank_rects,
padding_width,
border_width,
draw_window_borders=True,
):
add_borders_rect(self.os_window_id, self.tab_id, 0, 0, 0, 0, BorderColor.default_bg)
@@ -68,7 +68,7 @@ class Borders:
if not has_background_image:
for br in chain(current_layout.blank_rects, extra_blank_rects):
add_borders_rect(self.os_window_id, self.tab_id, *br, BorderColor.default_bg)
bw, pw = self.border_width, self.padding_width
bw, pw = border_width, padding_width
if bw + pw <= 0:
return
draw_borders = bw > 0 and draw_window_borders