[ivette/wp] TIP switch

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}

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} />
     </>
   );
 }

ivette/src/frama-c/plugins/wp/tip.tsx

+/* ************************************************************************ */
+/*                                                                          */
+/*   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>
+  );
+}
+
+/* -------------------------------------------------------------------------- */