ui.backend.gtk: Save the clipboard to the global clipboard so that it doesn't get...

diff --git a/basis/ui/backend/gtk/gtk.factor b/basis/ui/backend/gtk/gtk.factor
index b4c4225a9c9c34ec1266dffc0ec56acbb07cbd41..64e53a6a6128d138128b040684e802cf74303f00 100644 (file)
--- a/basis/ui/backend/gtk/gtk.factor
+++ b/basis/ui/backend/gtk/gtk.factor
@@ -42,9 +42,13 @@ M: gtk-clipboard clipboard-contents
         [ &g_free utf8 alien>string ] [ f ] if*
     ] with-destructors ;
 
+: save-global-clipboard ( -- )
+    clipboard get-global handle>> gtk_clipboard_store ;
+
 M: gtk-clipboard set-clipboard-contents
     swap [ handle>> ] [ utf8 string>alien ] bi*
-    -1 gtk_clipboard_set_text ;
+    -1 gtk_clipboard_set_text
+    save-global-clipboard ;
 
 : init-clipboard ( -- )
     selection "PRIMARY"

diff --git a/basis/ui/gadgets/editors/editors.factor b/basis/ui/gadgets/editors/editors.factor
index ad4cf6b77b19bb229a1b307a8ab9ca56c48ac4c1..ab385d48d058d6a23a932c3ed04eae0b2d75ae06 100644 (file)
--- a/basis/ui/gadgets/editors/editors.factor
+++ b/basis/ui/gadgets/editors/editors.factor
@@ -499,6 +499,7 @@ editor "selection" f {
     } show-commands-menu ;
 
 editor "misc" f {
+    ! { T{ button-down f f 2 } paste-selection }
     { T{ button-down f f 3 } editor-menu }
 } define-command-map