linuxmint/Cinnamon — pull request #1537 by plaa (2012-12-24 12:23:17+00:00)
Title: Edge flip enhancements

This pull request includes two enhancements to the workspace edge flipping functionality:

1. The mouse pointer moves to the opposite edge of the screen when flipping. This is the natural way for edge flipping, as it emulates a long, continuous desktop.

2. The edge flip delay is configurable. I was testing using patches against the version of Cinnamon in Linux Mint 14 and was unable to get the GUI settings configuration to display the option. Instead it is configured by the setting org.cinnamon/edge-flip-delay. (You can set it with "gsettings set org.cinnamon edge-flip-delay 100".) The place to add the configuration is in cs_windows.py.

Since edgeFlip.js polls for the mouse pointer hitting the edge of the screen, the logic is the following:
- poll every edge-flip-delay/2 milliseconds, but at most every 200 ms (to prevent too much power usage on laptops)
- when the pointer hits the edge, delay edge-flip-delay milliseconds before flipping