If we use the current view position to calculate the destination for a scroll event, then we may effectively lose the difference between view.pos and scroll_dest if we are still animating a scroll when the new event arrives. This can happen when scroll events are received really quickly which can happen with some devices like touchpads or fast scroll wheels. Now we use the scroll_dest which means that we extend the destination for animated scrolling instead of overwriting it. |
||
|---|---|---|
| .. | ||
| mode | ||
| status | ||
| Box.zig | ||
| Button.zig | ||
| editor.zig | ||
| editor_gutter.zig | ||
| expansion.zig | ||
| filelist_view.zig | ||
| Fire.zig | ||
| fonts.zig | ||
| home.zig | ||
| info_view.zig | ||
| InputBox.zig | ||
| inputview.zig | ||
| inspector_view.zig | ||
| keybindview.zig | ||
| keyhints.zig | ||
| logview.zig | ||
| lsp_info.zig | ||
| mainview.zig | ||
| Menu.zig | ||
| MessageFilter.zig | ||
| ModalBackground.zig | ||
| scrollbar_v.zig | ||
| tui.zig | ||
| Widget.zig | ||
| WidgetList.zig | ||
| WidgetStack.zig | ||
| WidgetStyle.zig | ||