Maximum font size for margin text should be the body font size not hardcoded to 12px

This commit is contained in:
Kovid Goyal 2020-03-09 15:40:36 +05:30
parent 0ada2ad42b
commit 948a15965e
No known key found for this signature in database
GPG Key ID: 06BC317B515ACE7C

View File

@ -127,9 +127,23 @@ def show_controls_help():
# }}} # }}}
def maximum_font_size():
ans = maximum_font_size.ans
if not ans:
q = window.getComputedStyle(document.body).fontSize
if q and q.endsWith('px'):
q = parseInt(q)
if q and not isNaN(q):
ans = maximum_font_size.ans = q
return ans
ans = maximum_font_size.ans = 12
return ans
def margin_elem(sd, which, id, onclick, oncontextmenu): def margin_elem(sd, which, id, onclick, oncontextmenu):
sz = sd.get(which, 20) sz = sd.get(which, 20)
fsz = min(max(0, sz - 6), 12) fsz = min(max(0, sz - 6), maximum_font_size())
s = '; text-overflow: ellipsis; white-space: nowrap; overflow: hidden' s = '; text-overflow: ellipsis; white-space: nowrap; overflow: hidden'
ans = E.div( ans = E.div(
style=f'height:{sz}px; overflow: hidden; font-size:{fsz}px; width:100%; padding: 0; display: flex; justify-content: space-between; align-items: center', style=f'height:{sz}px; overflow: hidden; font-size:{fsz}px; width:100%; padding: 0; display: flex; justify-content: space-between; align-items: center',