[ivette/wp] view labels & titles

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

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