adjust font sizes in response to zoom changes

akkartik

Jan 1, 2024, 1:40 AM

DEFJUKUVTIPCGXEZ5Q7SBCIXREZRWDRQLSBHXY7PGHVGR3UWOCUAC

Dependencies

• [2] GVX7YSQY initial script after splitting up text-zoom

Change contents

• replacement in screens/text-box at line 123
  [2.4723]→[2.4723:4826](∅→∅)
  − local update_font = function(newf)

  − if font_height == newf then return end

  − font_height = newf
  [2.4723]

  [2.4826]
  + r.refresh_font = function()
• edit in screens/text-box at line 129
  [2.4977]

  [2.4977]
  + local update_font = function(newf)

  + if font_height == newf then return end

  + font_height = newf

  + r.refresh_font()

  + end
• edit in screens/main at line 68
  [2.8135]

  [2.8135]
  + for _,w in ipairs(widgets) do

  + if w.refresh_font then w.refresh_font() end

  + end