switch_to_next_workspace: require timestamp (#1830)

This commit is contained in:
Leo 2024-01-18 19:24:49 +09:00 committed by GitHub
parent a6de96702c
commit 15ef7cf3d6
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 10 additions and 9 deletions

View File

@ -180,6 +180,6 @@ namespace Gala {
*
* @param direction The direction in which to switch
*/
public abstract void switch_to_next_workspace (Meta.MotionDirection direction);
public abstract void switch_to_next_workspace (Meta.MotionDirection direction, uint32 timestamp);
}
}

View File

@ -479,7 +479,7 @@ namespace Gala {
private void handle_switch_to_workspace (Meta.Display display, Meta.Window? window,
Clutter.KeyEvent event, Meta.KeyBinding binding) {
var direction = (binding.get_name () == "switch-to-workspace-left" ? Meta.MotionDirection.LEFT : Meta.MotionDirection.RIGHT);
switch_to_next_workspace (direction);
switch_to_next_workspace (direction, event.get_time ());
}
[CCode (instance_pos = -1)]
@ -537,6 +537,8 @@ namespace Gala {
return;
}
unowned var display = get_display ();
var fingers = gesture.fingers;
var three_finger_swipe_horizontal = GestureSettings.get_string ("three-finger-swipe-horizontal");
@ -554,13 +556,12 @@ namespace Gala {
switch_workspace_with_gesture = three_fingers_switch_to_workspace || four_fingers_switch_to_workspace;
if (switch_workspace_with_gesture) {
var direction = gesture_tracker.settings.get_natural_scroll_direction (gesture);
switch_to_next_workspace (direction);
switch_to_next_workspace (direction, display.get_current_time ());
return;
}
switch_workspace_with_gesture = three_fingers_move_to_workspace || four_fingers_move_to_workspace;
if (switch_workspace_with_gesture) {
unowned var display = get_display ();
unowned var manager = display.get_workspace_manager ();
var direction = gesture_tracker.settings.get_natural_scroll_direction (gesture);
@ -570,7 +571,7 @@ namespace Gala {
moving.change_workspace (manager.get_active_workspace ().get_neighbor (direction));
}
switch_to_next_workspace (direction);
switch_to_next_workspace (direction, display.get_current_time ());
return;
}
@ -583,7 +584,7 @@ namespace Gala {
/**
* {@inheritDoc}
*/
public void switch_to_next_workspace (Meta.MotionDirection direction) {
public void switch_to_next_workspace (Meta.MotionDirection direction, uint32 timestamp) {
if (animating_switch_workspace) {
return;
}
@ -593,7 +594,7 @@ namespace Gala {
unowned var neighbor = active_workspace.get_neighbor (direction);
if (neighbor != active_workspace) {
neighbor.activate (display.get_current_time ());
neighbor.activate (timestamp);
} else {
// if we didn't switch, show a nudge-over animation if one is not already in progress
if (workspace_view.is_opened () && workspace_view is MultitaskingView) {
@ -981,10 +982,10 @@ namespace Gala {
current.stick ();
break;
case ActionType.SWITCH_TO_WORKSPACE_PREVIOUS:
switch_to_next_workspace (Meta.MotionDirection.LEFT);
switch_to_next_workspace (Meta.MotionDirection.LEFT, Gtk.get_current_event_time ());
break;
case ActionType.SWITCH_TO_WORKSPACE_NEXT:
switch_to_next_workspace (Meta.MotionDirection.RIGHT);
switch_to_next_workspace (Meta.MotionDirection.RIGHT, Gtk.get_current_event_time ());
break;
case ActionType.MOVE_CURRENT_WORKSPACE_LEFT:
unowned var workspace_manager = get_display ().get_workspace_manager ();