From 21f44fb1b0f6bd8d82fe253ba2d0359917545861 Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime2.jacquemin@gmail.com>
Date: Mon, 16 Jan 2023 16:55:57 +0100
Subject: [PATCH] [Ivette] Fix the scrolling on selection in SourceCode
---
ivette/src/dome/renderer/text/editor.tsx | 5 +++-
ivette/src/frama-c/kernel/SourceCode.tsx | 31 ++++++++++++++++--------
2 files changed, 25 insertions(+), 11 deletions(-)
diff --git a/ivette/src/dome/renderer/text/editor.tsx b/ivette/src/dome/renderer/text/editor.tsx
index 1dd6f7758ba..15d4be789fe 100644
--- a/ivette/src/dome/renderer/text/editor.tsx
+++ b/ivette/src/dome/renderer/text/editor.tsx
@@ -363,13 +363,16 @@ export function unfoldAll(view: View): void {
}
// Move to the given line. The indexation starts at 1.
-export function selectLine(view: View, line: number): void {
+export function selectLine(view: View, line: number, atTop: boolean): void {
if (!view || view.state.doc.lines < line) return;
const doc = view.state.doc;
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({ effects });
}
// -----------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index e945a690069..b099a503816 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -165,23 +165,31 @@ const extensions: Editor.Extension[] = [
EventsHandler,
];
+function markerLocation(m: Ast.marker | undefined): Ast.source | undefined {
+ const markersInfo = States.useSyncArray(Ast.markerInfo);
+ if (m === undefined || m === '') return undefined;
+ return markersInfo.getData(m)?.sloc;
+}
+
+function functionLocation(fct: string | undefined): Ast.source | undefined {
+ const functionsData = States.useSyncArray(Ast.functions).getArray();
+ if (fct === undefined || fct === '') return undefined;
+ return functionsData.find((e) => e.name === fct)?.sloc;
+}
+
// The component in itself.
export default function SourceCode(): JSX.Element {
const [fontSize] = Settings.useGlobalSettings(Preferences.EditorFontSize);
const [command] = Settings.useGlobalSettings(Preferences.EditorCommand);
const { view, Component } = Editor.Editor(extensions);
- const functionsData = States.useSyncArray(Ast.functions).getArray();
- const markersInfo = States.useSyncArray(Ast.markerInfo);
const [selection, updateSelection] = States.useSelection();
const marker = selection?.current?.marker;
const fct = selection?.current?.fct;
+ const displayedFct = React.useRef<string | undefined>(undefined);
- const markerSloc =
- (marker && marker !== '') ? markersInfo.getData(marker)?.sloc : undefined;
- const fctSloc = fct && functionsData.find((e) => e.name === fct)?.sloc;
- const sloc = markerSloc ?? fctSloc;
- const file = sloc ? sloc.file : '';
- const line = sloc ? sloc.line : undefined;
+ const markerSloc = markerLocation(marker);
+ const fctSloc = functionLocation(fct);
+ const file = fctSloc?.file ?? '';
const filename = Path.parse(file).base;
Source.set(view, useFctSource(file));
@@ -190,8 +198,11 @@ export default function SourceCode(): JSX.Element {
File.set(view, file);
React.useEffect(() => {
- if (line) Editor.selectLine(view, line);
- }, [view, line]);
+ const notDisplayedFct = fct !== displayedFct.current;
+ const line = notDisplayedFct ? fctSloc?.line : markerSloc?.line;
+ if (line) Editor.selectLine(view, line, notDisplayedFct);
+ displayedFct.current = fct;
+ }, [view, markerSloc, fctSloc, displayedFct, fct]);
const externalEditorTitle =
'Open the source file in an external editor.\nA Ctrl-click '
--
GitLab