From a5dd7213ba09a467c84ba83001e9819f45095a87 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 23 Mar 2022 14:24:15 +0100
Subject: [PATCH] [ivette] Marker info: a meta selection pins the selected
marker.
---
ivette/src/frama-c/kernel/ASTinfo.tsx | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/ivette/src/frama-c/kernel/ASTinfo.tsx b/ivette/src/frama-c/kernel/ASTinfo.tsx
index 176801ed0f6..5453dc220c1 100644
--- a/ivette/src/frama-c/kernel/ASTinfo.tsx
+++ b/ivette/src/frama-c/kernel/ASTinfo.tsx
@@ -324,6 +324,13 @@ export default function ASTinfo(): JSX.Element {
React.useEffect(() => {
markers.setLocations(selectedLoc, hoveredLoc);
}, [markers, selectedLoc, hoveredLoc]);
+ const pinMarker = (location: States.Location) : void => {
+ markers.setPinned(location?.marker, true);
+ };
+ React.useEffect(() => {
+ States.MetaSelection.on(pinMarker);
+ return () => States.MetaSelection.off(pinMarker);
+ });
// Rendering
const renderMark = (mark: Mark): JSX.Element | null => {
const { marker } = mark;
--
GitLab