support undo of paste button

akkartik

Dec 2, 2023, 4:22 AM

X2DGB56U45XYFJNGFZ2PPXYR63BMGFSDJFCE2CWFRMSZFDR253HAC

Dependencies

• [2] SIJ5I4NZ extract a helper for buttons
• [3] 5MEJ7XNH lay out buttons based on device dimensions
• [4] RK2ASPN7 add lots of buttons to the toolbar

Change contents

• edit in 0067-paste_button at line 4
  [2.842]

  [3.4071]
  + local state = Current_pane.editor_state

  + -- initial state for recording undo operation

  + local before_line = state.cursor1.line

  + local before = snapshot(state, before_line)

  + -- paste
• replacement in 0067-paste_button at line 10
  [3.4104]→[3.4104:4154](∅→∅)
  − Text.insert_text(Current_pane.editor_state, s)
  [3.4104]

  [2.843]
  + Text.insert_text(state, s)

  + -- record undo operation

  + record_undo_event(state,

  + {

  + before=before,

  + after=snapshot(

  + state, before_line,

  + state.cursor1.line)

  + })
• replacement in 0067-paste_button at line 20
  [2.850]→[3.4180:4183](∅→∅),[3.2707]→[3.4180:4183](∅→∅),[3.4180]→[3.4180:4183](∅→∅)
  − end
  [2.850]
  + end