From c46d61a82b311dfd6ed4d73b00df1bfe2945ab17 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 24 Mar 2023 20:56:07 +0100
Subject: [PATCH] [Ivette] Shows a message in the status bar when multiple
markers are selected.
---
ivette/src/frama-c/states.ts | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 01ff09edb8a..8f3e5342f93 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -38,6 +38,7 @@ import { Client, useModel } from 'dome/table/models';
import { CompactModel } from 'dome/table/arrays';
import * as Ast from 'frama-c/kernel/api/ast';
import * as Server from './server';
+import * as Status from 'frama-c/kernel/Status';
// --------------------------------------------------------------------------
// --- Pretty Printing (Browser Console)
@@ -789,6 +790,14 @@ export function useSelection(): [Selection, (a: SelectionActions) => void] {
const [current, setCurrent] = useGlobalState(GlobalSelection);
const callback = React.useCallback((action) => {
setCurrent(reducer(current, action));
+ if (isMultipleSelect(action)) {
+ const l = action.locations.length;
+ const markers =
+ (l > 1) ? `${l} markers selected, listed in the 'Locations' panel` :
+ (l === 1) ? `1 marker selected` : `no markers selected`;
+ const text = `${action.name}: ${markers}`;
+ Status.setMessage({ text, title: action.title, kind: 'success' });
+ }
}, [current, setCurrent]);
return [current, callback];
}
--
GitLab