bugfix: update output font (and menus)

akkartik

Dec 31, 2023, 5:26 AM

OTJQKAQZ4QXHLLAC3JROQ4HI3RFL2IWB54KG6UUDNICNYB3KNU4AC

Dependencies

• [2] UUAIVZ4U 2 bugfixes in font rendering
• [3] IUOZ4YHC use the obvious name for the font global
• [4] FQAZKPOO bugfix: infinite loop if window is too narrow
• [5] IQW6KIIL bugfix: changing font size
• [6] OE26XIQO bring back syntax highlighting (but so ugly)
• [7] YV2GBDNW preserve settings across restart
• [8] PRE6XPRN responsively increase/decrease font height

Change contents

• edit in 0032-update_font_settings at line 3
  [4.934]

  [3.0]
  + Line_height = math.floor(Font_height*1.3)
• edit in 0032-update_font_settings at line 6
  [3.72]→[4.935:978](∅→∅),[4.215]→[4.935:978](∅→∅),[4.155]→[4.935:978](∅→∅)
  − Line_height = math.floor(font_height*1.3)
• replacement in 0032-update_font_settings at line 17
  [4.1016]→[4.1016:1076](∅→∅)
  − edit.update_font_settings(pane.editor_state, font_height)
  [4.1016]

  [4.1076]
  + edit.update_font_settings(pane.editor_state, Font_height)
• edit in 0032-update_font_settings at line 19
  [4.1113]

  [2.367]
  + edit.update_font_settings(pane.output_editor_state, Font_height)