ExternalTools: Maintain scroll position on doc reload
When document is reloaded we loose our existing scroll position and the cursor is recentered. Try to avoid that so that it looks more smooth and less jumpy.
When document is reloaded we loose our existing scroll position and the cursor is recentered. Try to avoid that so that it looks more smooth and less jumpy.