From 520ea326d2d3e263cf3a884cc0c8093b6f9cbc0f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Sat, 25 Mar 2023 11:22:01 +0100
Subject: [PATCH] [Ivette] Improves editor scrolling in SourceCode and ASTview.
Scroll to center selected element, but only if it is not already visible.
---
ivette/src/dome/renderer/text/editor.tsx | 19 ++++++++++++++++---
ivette/src/frama-c/kernel/ASTview.tsx | 3 ++-
2 files changed, 18 insertions(+), 4 deletions(-)
diff --git a/ivette/src/dome/renderer/text/editor.tsx b/ivette/src/dome/renderer/text/editor.tsx
index 7ca40b680eb..c22c6f6835c 100644
--- a/ivette/src/dome/renderer/text/editor.tsx
+++ b/ivette/src/dome/renderer/text/editor.tsx
@@ -432,6 +432,18 @@ export function unfoldAll(view: View): void {
if (view !== null) Language.unfoldAll(view);
}
+function isVisible(view: View, line: number): boolean {
+ if (!view || view.state.doc.lines < line) return false;
+ const doc = view.state.doc;
+ const top = view.documentTop;
+ const rect = view.dom.getBoundingClientRect();
+ const topVisibleBlock = view.lineBlockAtHeight(rect.top - top);
+ const topVisibleLine = doc.lineAt(topVisibleBlock.to).number;
+ const bottomVisibleBlock = view.lineBlockAtHeight(rect.bottom - top);
+ const bottomVisibleLine = doc.lineAt(bottomVisibleBlock.from).number;
+ return (topVisibleLine < line && line < bottomVisibleLine);
+}
+
// Move to the given line. The indexation starts at 1.
export function selectLine(view: View, line: number, atTop: boolean): void {
if (!view || view.state.doc.lines < line) return;
@@ -439,9 +451,10 @@ export function selectLine(view: View, line: number, atTop: boolean): void {
const { from: here } = doc.lineAt(view.state.selection.main.from);
const { from: goto } = doc.line(Math.max(line, 1));
if (here === goto) return;
- view.dispatch({ selection: { anchor: goto }, scrollIntoView: true });
- if (!atTop) return;
- const effects = EditorView.scrollIntoView(goto, { y: 'start', yMargin: 0 });
+ view.dispatch({ selection: { anchor: goto } });
+ if (isVisible(view, line)) return;
+ const verticalScroll = atTop ? 'start' : 'center';
+ const effects = EditorView.scrollIntoView(goto, { y: verticalScroll });
view.dispatch({ effects });
}
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index 112823a87b6..94b20dc6b61 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -217,7 +217,8 @@ function createMarkerScroller(): Editor.Extension {
const markerRanges = ranges.get(marker) ?? [];
if (markerRanges.length !== 1) return;
const { from: anchor } = markerRanges[0];
- view.dispatch({ selection: { anchor }, scrollIntoView: true });
+ const line = view.state.doc.lineAt(anchor).number;
+ Editor.selectLine(view, line, false);
});
}
--
GitLab