CodeMirror is set to expand so that it doesn't have a scroll bar, but it usually fails and the observed behaviour is that it has a scroll bar, but when you scroll, the scroll bar disappears.
We can probably get rid of this by forcing CodeMirror to refresh well after the page is fully loaded, like with a setTimeout call.
Aggressively applying and re-applying refresh() even after waiting intervals seems to be ineffective against this issue. Counting this as a point for ditching Code Mirror.
CodeMirror is set to expand so that it doesn't have a scroll bar, but it usually fails and the observed behaviour is that it has a scroll bar, but when you scroll, the scroll bar disappears.
We can probably get rid of this by forcing CodeMirror to refresh well after the page is fully loaded, like with a setTimeout call.