From fe441e9f4f11dc9835fdedbc6f80291d4364564f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 5 Apr 2023 14:59:39 +0200
Subject: [PATCH] [ivette] proposal for property filter summary
---
ivette/src/frama-c/kernel/Properties.tsx | 11 ++++++-----
1 file changed, 6 insertions(+), 5 deletions(-)
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index 4cbb8f9919c..d458118d53d 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -142,7 +142,9 @@ function filterSummary(prefix: string) : string {
if (filter(key)) enabled++;
}
}
- return `${enabled} / ${total}`;
+ if (enabled == 0) return '(none)';
+ if (enabled == total) return '(all)';
+ return `(${enabled}/${total})`;
}
function filterStatus(
@@ -416,7 +418,7 @@ async function onContextMenu(prefix:string): Promise<void> {
function FilterSection(props: SectionProps): JSX.Element {
const settings = `properties-section-${props.label}`;
- const { prefix } = props;
+ const { label, prefix } = props;
const filterButtonProps =
prefix ? {
icon: 'TUNINGS',
@@ -425,14 +427,13 @@ function FilterSection(props: SectionProps): JSX.Element {
} : undefined;
const update = Dome.useForceUpdate();
Settings.useWindowSettingsEvent(update);
- const summary = prefix ? filterSummary(prefix) : undefined;
+ const theLabel = prefix ? `${label} ${filterSummary(prefix)}` : label;
return (
<Section
- label={props.label}
+ label={theLabel}
settings={settings}
defaultUnfold={props.unfold}
rightButtonProps={filterButtonProps}
- summary={summary}
>
{props.children}
</Section>
--
GitLab