Implement Post Selection Provider [was #7488]
{color:red}
reported by [~wissenbach] at 2008-01-11
previously known as [trac#23|http://www.textgrid.de/trac/ticket/23] {color}
Implement Post Selection Provider, which means that the selected element is only propagated after you do not move the cursor for so long.
Should make for smoother moving around.