2023-11-22 20:38:16 +00:00
|
|
|
paste_button = function(x, y, r)
|
2023-11-26 05:11:24 +00:00
|
|
|
return overflowable_button('paste', x, y, r,
|
|
|
|
function()
|
2023-12-05 06:09:47 +00:00
|
|
|
Show_menu = nil
|
2023-12-02 04:22:27 +00:00
|
|
|
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
|
2023-11-21 06:23:09 +00:00
|
|
|
local s = App.get_clipboard()
|
2023-12-02 04:22:27 +00:00
|
|
|
Text.insert_text(state, s)
|
|
|
|
-- record undo operation
|
|
|
|
record_undo_event(state,
|
|
|
|
{
|
|
|
|
before=before,
|
|
|
|
after=snapshot(
|
|
|
|
state, before_line,
|
|
|
|
state.cursor1.line)
|
|
|
|
})
|
2023-11-26 05:11:24 +00:00
|
|
|
end)
|
2023-12-05 06:09:47 +00:00
|
|
|
end
|