From 584f7238e30ca4ea39b9423f0154051326ee3c8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 30 Nov 2023 19:13:12 +0100
Subject: [PATCH] [ivette/wp] TIP switch
---
ivette/src/frama-c/plugins/wp/goals.tsx | 13 ++++++--
ivette/src/frama-c/plugins/wp/index.tsx | 36 ++++++++++++++++------
ivette/src/frama-c/plugins/wp/tip.tsx | 40 +++++++++++++++++++++++++
3 files changed, 77 insertions(+), 12 deletions(-)
create mode 100644 ivette/src/frama-c/plugins/wp/tip.tsx
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index b0d5085ce4b..1155150d55d 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -33,7 +33,7 @@ import * as WP from 'frama-c/plugins/wp/api';
/* -------------------------------------------------------------------------- */
function getScope(g : WP.goalsData): string {
- if (g.bhv && g.fct) return `${g.fct}@{g.bhv}}`;
+ if (g.bhv && g.fct) return `${g.fct} — {g.bhv}}`;
if (g.fct) return g.fct;
if (g.thy) return g.thy;
return '';
@@ -94,11 +94,12 @@ function filterGoal(
/* -------------------------------------------------------------------------- */
export interface GoalTableProps {
+ display: boolean;
scope: Ast.decl | undefined;
failed: boolean;
- display: boolean;
current: WP.goal;
setCurrent: (goal: WP.goal) => void;
+ setTIP: (goal: WP.goal) => void;
setGoals: (goals: number) => void;
setTotal: (total: number) => void;
}
@@ -106,7 +107,7 @@ export interface GoalTableProps {
export function GoalTable(props: GoalTableProps): JSX.Element {
const {
display, scope, failed,
- current, setCurrent,
+ current, setCurrent, setTIP,
setGoals, setTotal,
} = props;
const { model } = States.useSyncArrayProxy(WP.goals);
@@ -117,6 +118,11 @@ export function GoalTable(props: GoalTableProps): JSX.Element {
States.setSelected(marker);
setCurrent(wpo);
}, [setCurrent]);
+ const onDoubleClick = React.useCallback(
+ ({ wpo }: WP.goalsData) => {
+ setTIP(wpo);
+ }, [setTIP]
+ );
React.useEffect(() => {
if (failed || !!scope) {
@@ -136,6 +142,7 @@ export function GoalTable(props: GoalTableProps): JSX.Element {
settings='wp.goals'
selection={current}
onSelection={onSelection}
+ onDoubleClick={onDoubleClick}
>
<Column id='scope' label='Scope'
width={150}
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index 130396a3d38..ac06fc2a954 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -31,8 +31,10 @@ import { IconButton } from 'dome/controls/buttons';
import { LED, Meter } from 'dome/controls/displays';
import { Group, Inset } from 'dome/frame/toolbars';
import * as Ivette from 'ivette';
+import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
import { GoalTable } from './goals';
+import { TIP } from './tip';
import * as WP from 'frama-c/plugins/wp/api';
import './style.css';
@@ -43,11 +45,15 @@ import './style.css';
function WPGoals(): JSX.Element {
const [scoped, flipScoped] = Dome.useFlipSettings('frama-c.wp.goals.scoped');
const [failed, flipFailed] = Dome.useFlipSettings('frama-c.wp.goals.failed');
+ const [tip, flipTip] = Dome.useFlipSettings('frama-c.wp.goals.tip', false);
const [current, setCurrent] = React.useState(WP.goalDefault);
+ Server.useShutdown(() => setCurrent(WP.goalDefault));
const scope = States.useCurrentScope();
const [goals, setGoals] = React.useState(0);
const [total, setTotal] = React.useState(0);
const hasGoals = total > 0;
+ const hasSelection = current !== WP.goalDefault;
+ const displayTip = tip && hasSelection;
return (
<>
<Ivette.TitleBar>
@@ -55,24 +61,36 @@ function WPGoals(): JSX.Element {
{goals} / {total}
</Label>
<Inset />
- <IconButton icon='CURSOR' title='Current Scope Only'
- enabled={hasGoals}
- selected={scoped}
- onClick={flipScoped} />
- <IconButton icon='CIRC.QUESTION' title='Unresolved Goals Only'
- enabled={hasGoals}
- selected={failed}
- onClick={flipFailed} />
+ <IconButton
+ icon='CURSOR' title='Current Scope Only'
+ enabled={hasGoals}
+ selected={scoped}
+ onClick={flipScoped} />
+ <IconButton
+ icon='CIRC.QUESTION' title='Unresolved Goals Only'
+ enabled={hasGoals}
+ selected={failed}
+ onClick={flipFailed} />
+ <IconButton
+ icon={displayTip ? 'ITEMS.LIST' : 'MEDIA.PLAY'}
+ kind={displayTip ? 'warning' : 'positive'}
+ title='Goal Resolution'
+ enabled={hasSelection}
+ onClick={flipTip} />
</Ivette.TitleBar>
<GoalTable
- display={true}
+ display={!displayTip}
scope={scope}
failed={failed}
current={current}
setCurrent={setCurrent}
+ setTIP={flipTip}
setGoals={setGoals}
setTotal={setTotal}
/>
+ <TIP
+ display={displayTip}
+ goal={current} />
</>
);
}
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
new file mode 100644
index 00000000000..af1dafa4fe8
--- /dev/null
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -0,0 +1,40 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/* ************************************************************************ */
+
+import React from 'react';
+import { Vfill } from 'dome/layout/boxes';
+import * as WP from 'frama-c/plugins/wp/api';
+export interface TIPProps {
+ display: boolean;
+ goal: WP.goal;
+}
+
+export function TIP(props: TIPProps): JSX.Element {
+ const { display, goal } = props;
+ return (
+ <Vfill display={display}>
+ <div>{goal}</div>
+ </Vfill>
+ );
+}
+
+/* -------------------------------------------------------------------------- */
--
GitLab