2023-11-22 20:38:16 +00:00
|
|
|
copy_button = function(x, y, r)
|
2023-11-26 05:11:24 +00:00
|
|
|
return overflowable_button('copy', x, y, r,
|
|
|
|
function()
|
2023-12-05 06:09:47 +00:00
|
|
|
Show_menu = nil
|
2023-11-24 00:20:37 +00:00
|
|
|
local e = Current_pane.editor_state
|
|
|
|
local s = Text.selection(e)
|
|
|
|
if s == nil then
|
|
|
|
-- nothing selected? copy entire editor
|
|
|
|
-- workaround while we have no way to save to file
|
|
|
|
e.selection1 = {line=1, pos=1}
|
|
|
|
e.cursor1 = {line=#e.lines, pos=utf8.len(e.lines[#e.lines].data)+1}
|
|
|
|
s = Text.selection(e)
|
|
|
|
end
|
|
|
|
App.set_clipboard(s)
|
2023-11-26 05:11:24 +00:00
|
|
|
end)
|
2023-12-05 06:09:47 +00:00
|
|
|
end
|