make print _much_ more efficient

akkartik

Sep 27, 2024, 4:17 AM

2SE2CRDRZYSNDLVDE4WV7OQATB4IPFLGH44XB2YM6EUMVH3UFL4QC

Dependencies

• [2] 5OCELN37 bugfix in output editor wrapping
• [3] 4HCP3NTO draw code editor after menu and output
• [4] I52S4E5F running `print` now appends to output editor
• [5] YK5FRJWH print to output buffer in all callbacks
• [6] 7SJHYHMB clean up the setFont gotcha
• [*] ZM7NOBRM new fork: carousel shell

Change contents

• edit in 0050-print_to_output at line 5
  [2.59]→[4.190:241](∅→∅),[4.1566]→[4.190:241](∅→∅)
  − Text.redraw_all(Current_pane.output_editor_state)
• edit in 0012-on.draw at line 19
  [3.37]

  [3.37]
  + if #Current_pane.output_editor_state.lines ~= #Current_pane.output_editor_state.line_cache then

  + Text.redraw_all(Current_pane.output_editor_state)

  + end