ui.backend.gtk: add handling of insert key (#1656)

diff --git a/basis/ui/backend/gtk/gtk.factor b/basis/ui/backend/gtk/gtk.factor
index e1616b5f34664fe5c3844861739b159326d39422..7f75dfd4e8c65f135448be547cbca74656ca0258 100644 (file)
--- a/basis/ui/backend/gtk/gtk.factor
+++ b/basis/ui/backend/gtk/gtk.factor
@@ -113,6 +113,7 @@ CONSTANT: action-key-codes
         { $ GDK_KEY_KP_Enter "ENTER" }
         { $ GDK_KEY_Escape "ESC" }
         { $ GDK_KEY_Delete "DELETE" }
+        { $ GDK_KEY_Insert "INSERT" }
         { $ GDK_KEY_Home "HOME" }
         { $ GDK_KEY_Left "LEFT" }
         { $ GDK_KEY_Up "UP" }
@@ -197,8 +198,9 @@ CONSTANT: action-key-codes
     ] dip window send-scroll t ;
 
 : key-sym ( event -- sym/f action? )
-    keyval>> dup action-key-codes at [ t ]
-    [ gdk_keyval_to_unicode [ f ] [ 1string ] if-zero f ] ?if ;
+    keyval>> dup action-key-codes at [ t ] [
+        gdk_keyval_to_unicode [ f ] [ 1string ] if-zero f
+    ] ?if ;
 
 : key-event>gesture ( event -- key-gesture )
     [ event-modifiers ] [ key-sym ] [