From 5b8b067d8e48d6b58ffebb0123ab0ea428a7b506 Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Thu, 28 Apr 2022 14:26:38 +0200
Subject: [PATCH] [ivette] Resolve duplicate menu items warning for the
Evaluation mode
---
ivette/src/frama-c/plugins/eva/valuetable.tsx | 17 +++++++++--------
1 file changed, 9 insertions(+), 8 deletions(-)
diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx
index 00c3b7738ba..5f0aef4d0a9 100644
--- a/ivette/src/frama-c/plugins/eva/valuetable.tsx
+++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx
@@ -914,6 +914,15 @@ interface EvaluationModeProps {
setLocPin: (loc: Location, pin: boolean) => void;
}
+Dome.addMenuItem({
+ menu: 'Edit',
+ id: 'EvaluateMenu',
+ type: 'normal',
+ label: 'Evaluate',
+ key: 'Cmd+E',
+ onClick: () => evaluateEvent.emit(),
+});
+
function useEvaluationMode(props: EvaluationModeProps): void {
const { computationState, selection, setLocPin } = props;
const handleError = (): void => { return; };
@@ -941,14 +950,6 @@ function useEvaluationMode(props: EvaluationModeProps): void {
Toolbars.RegisterMode.emit(evalMode);
return () => Toolbars.UnregisterMode.emit(evalMode);
});
- Dome.addMenuItem({
- menu: 'Edit',
- id: 'EvaluateMenu',
- type: 'normal',
- label: 'Evaluate',
- key: 'Cmd+E',
- onClick: () => evaluateEvent.emit(),
- });
React.useEffect(() => {
Dome.setMenuItem({ id: 'EvaluateMenu', enabled: true });
return () => Dome.setMenuItem({ id: 'EvaluateMenu', enabled: false });
--
GitLab