ui.backend.gtk: Save the clipboard to the global clipboard so that it doesn't get deleted when Factor exits. Fixes #548. Add paste-selection, but commented out for now.
parent
0c5d70e881
commit
1a5f2ad961
|
@ -42,9 +42,13 @@ M: gtk-clipboard clipboard-contents
|
||||||
[ &g_free utf8 alien>string ] [ f ] if*
|
[ &g_free utf8 alien>string ] [ f ] if*
|
||||||
] with-destructors ;
|
] with-destructors ;
|
||||||
|
|
||||||
|
: save-global-clipboard ( -- )
|
||||||
|
clipboard get-global handle>> gtk_clipboard_store ;
|
||||||
|
|
||||||
M: gtk-clipboard set-clipboard-contents
|
M: gtk-clipboard set-clipboard-contents
|
||||||
swap [ handle>> ] [ utf8 string>alien ] bi*
|
swap [ handle>> ] [ utf8 string>alien ] bi*
|
||||||
-1 gtk_clipboard_set_text ;
|
-1 gtk_clipboard_set_text
|
||||||
|
save-global-clipboard ;
|
||||||
|
|
||||||
: init-clipboard ( -- )
|
: init-clipboard ( -- )
|
||||||
selection "PRIMARY"
|
selection "PRIMARY"
|
||||||
|
|
|
@ -499,6 +499,7 @@ editor "selection" f {
|
||||||
} show-commands-menu ;
|
} show-commands-menu ;
|
||||||
|
|
||||||
editor "misc" f {
|
editor "misc" f {
|
||||||
|
! { T{ button-down f f 2 } paste-selection }
|
||||||
{ T{ button-down f f 3 } editor-menu }
|
{ T{ button-down f f 3 } editor-menu }
|
||||||
} define-command-map
|
} define-command-map
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue