From 5b54ebb06a339ec0f8f7b9ee47a27e6cd72f66f1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 4 Dec 2023 15:22:44 +0100
Subject: [PATCH] [ivette/wp] view labels & titles

---
 ivette/src/frama-c/plugins/wp/index.tsx | 22 ++++++++++++----------
 ivette/src/frama-c/plugins/wp/tip.tsx   | 11 ++++++-----
 2 files changed, 18 insertions(+), 15 deletions(-)

diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index 5e796766014..df58d4caa73 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -47,17 +47,19 @@ type Goal = WP.goal | undefined;
 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 [displayTip, setTip] = React.useState(false);
+  const [tip, setTip] = React.useState(false);
   const [current, setCurrent] = React.useState<Goal>(undefined);
   Server.useShutdown(() => { setTip(false); setCurrent(undefined); });
   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;
   return (
     <>
-      <Ivette.TitleBar>
+      <Ivette.TitleBar
+        label={tip ? 'WP — TIP' : 'WP — Goals'}
+        title={tip ? 'Interactive Proof Transformer' : 'Generated Goals'}
+      >
         <Label display={goals < total}>
           {goals} / {total}
         </Label>
@@ -73,14 +75,14 @@ function WPGoals(): JSX.Element {
           selected={failed}
           onClick={flipFailed} />
         <IconButton
-          icon={displayTip ? 'ITEMS.LIST' : 'MEDIA.PLAY'}
-          kind={displayTip ? 'warning' : 'positive'}
-          title='Goal Resolution'
-          enabled={hasSelection}
-          onClick={() => setTip(!displayTip)} />
+          icon={tip ? 'ITEMS.LIST' : 'MEDIA.PLAY'}
+          kind={tip ? 'warning' : 'positive'}
+          title={tip ? 'Back to Goals' : 'Interactive Proof Transformer'}
+          enabled={!!current}
+          onClick={() => setTip(!tip)} />
       </Ivette.TitleBar>
       <GoalTable
-        display={!displayTip}
+        display={!tip}
         scope={scope}
         failed={failed}
         current={current}
@@ -90,7 +92,7 @@ function WPGoals(): JSX.Element {
         setTotal={setTotal}
       />
       <TIPView
-        display={displayTip}
+        display={tip}
         goal={current} />
     </>
   );
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
index de8fa8d382d..1f4e3ceffd9 100644
--- a/ivette/src/frama-c/plugins/wp/tip.tsx
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -22,7 +22,8 @@
 
 import React from 'react';
 import { Cell } from 'dome/controls/labels';
-import { Vfill, Hbox } from 'dome/layout/boxes';
+import { ToolBar } from 'dome/frame/toolbars';
+import { Vfill } from 'dome/layout/boxes';
 import { MarkDecoration, Decorations, TextView } from 'dome/text/richtext';
 import * as States from 'frama-c/states';
 import * as RichText from 'frama-c/richtext';
@@ -145,16 +146,16 @@ export function TIPView(props: TIPProps): JSX.Element {
   const { current, index, pending } = useProofState(goal);
   return (
     <Vfill display={display}>
-      <Hbox>
+      <ToolBar>
         <Cell
           icon='HOME'
           label={infos.wpo} title='Goal identifier' />
         <Cell
           icon='CODE'
-          display={0 <= index && index < pending}
-          label={`${index}/${pending}`} title='Pending proof nodes'/>
+          display={0 <= index && index < pending && 1 < pending}
+          label={`${index+1}/${pending}`} title='Pending proof nodes'/>
         <Cell {...getStatus(infos)}/>
-      </Hbox>
+      </ToolBar>
       <GoalView node={current} />
     </Vfill>
   );
-- 
GitLab