Fixed scrolling issue

This commit is contained in:
Suzanne Soy 2023-11-21 17:56:32 +00:00
parent 10a2e6a01d
commit c80240e7f8

View File

@ -1177,7 +1177,12 @@ function ___scrollToLine(editor, line) {
editor.addLineClass(line, 'background', 'scrolled-to-line'); editor.addLineClass(line, 'background', 'scrolled-to-line');
var editorOffset = ___getOffset(editor.getScrollerElement()).top; var editorOffset = ___getOffset(editor.getScrollerElement()).top;
var lineOffset = editor.charCoords({line: line, ch: 0}, "local").top; var lineOffset = editor.charCoords({line: line, ch: 0}, "local").top;
document.body.scrollTo(0, editorOffset + lineOffset - window.innerHeight/2); var toOffset = editorOffset + lineOffset - window.innerHeight/2;
document.body.parentElement.scrollTo(0, toOffset);
if (document.body.parentElement.scrollTop == 0) {
// depending on the CSS, the scrollbar can belong to the HTML element or to the body element.
document.body.scrollTo(0, toOffset);
}
} }
function ___toCodeMirror(ta) { function ___toCodeMirror(ta) {
var editor = CodeMirror.fromTextArea(ta, { var editor = CodeMirror.fromTextArea(ta, {