From a5c17c0f60ca01f0285a29bb9bf342d3b2f0277a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 24 Mar 2022 10:30:36 +0100
Subject: [PATCH] [ivette] Marker info: do not show the 'remove' and 'pin'
buttons at the same time.
Only shows the 'remove' button when the marker is pinned and not selected
(if it is selected, it cannot be instantly removed).
Otherwise, shows the 'pin/unpin' button.
---
ivette/src/frama-c/kernel/ASTinfo.tsx | 22 ++++++++++------------
1 file changed, 10 insertions(+), 12 deletions(-)
diff --git a/ivette/src/frama-c/kernel/ASTinfo.tsx b/ivette/src/frama-c/kernel/ASTinfo.tsx
index 5453dc220c1..c1b688faec6 100644
--- a/ivette/src/frama-c/kernel/ASTinfo.tsx
+++ b/ivette/src/frama-c/kernel/ASTinfo.tsx
@@ -145,6 +145,15 @@ function MarkInfos(props: InfoSectionProps): JSX.Element {
const filtered = allInfos.filter((info) => !fs.some((m) => m === info.id));
const infos = more ? allInfos : filtered;
const hasMore = filtered.length < allInfos.length;
+ const pinButton =
+ (!props.pinned || props.selected) ?
+ {
+ icon: "PIN", selected: props.pinned, onClick: props.onPin,
+ title: "Pin/unpin marker information"
+ } : {
+ icon: "CIRC.CLOSE", onClick: props.onRemove,
+ title:"Remove marker information"
+ };
return (
<div
className={`astinfo-section ${highlight}`}
@@ -168,15 +177,6 @@ function MarkInfos(props: InfoSectionProps): JSX.Element {
<Code className="astinfo-markercode">
{kind}{descr}
</Code>
- <IconButton
- className="astinfo-markerbutton"
- title="Pin/unpin information in sidebar"
- size={9}
- offset={0}
- icon="PIN"
- selected={props.pinned}
- onClick={props.onPin}
- />
<IconButton
style={{ display: hasMore ? undefined : 'none' }}
className="astinfo-markerbutton"
@@ -189,11 +189,9 @@ function MarkInfos(props: InfoSectionProps): JSX.Element {
/>
<IconButton
className="astinfo-markerbutton"
- title="Remove informations"
size={9}
offset={0}
- icon="CIRC.CLOSE"
- onClick={props.onRemove}
+ {...pinButton}
/>
</div>
{unfold && infos.map((info) => <InfoItem key={info.id} {...info} />)}
--
GitLab