[ivette/wp] goal & list view

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

@@ -96,19 +96,27 @@ function filterGoal(
 export interface GoalTableProps {
   scope: Ast.decl | undefined;
   failed: boolean;
-  onFilter: (goals: number, total: number) => void;
+  display: boolean;
+  current: WP.goal;
+  setCurrent: (goal: WP.goal) => void;
+  setGoals: (goals: number) => void;
+  setTotal: (total: number) => void;
 }
 
 export function GoalTable(props: GoalTableProps): JSX.Element {
-  const { scope, failed, onFilter } = props;
-  const model = States.useSyncArrayModel(WP.goals);
-  const [wpoSelection, setWpoSelection] = React.useState(WP.goalDefault);
-
-  const onWpoSelection = React.useCallback(
+  const {
+    display, scope, failed,
+    current, setCurrent,
+    setGoals, setTotal,
+  } = props;
+  const { model } = States.useSyncArrayProxy(WP.goals);
+  const goals = model.getRowCount();
+  const total = model.getTotalRowCount();
+  const onSelection = React.useCallback(
     ({ wpo, property }: WP.goalsData) => {
       States.setSelected(property);
-      setWpoSelection(wpo);
-    }, []);
+      setCurrent(wpo);
+    }, [setCurrent]);
 
   React.useEffect(() => {
     if (failed || !!scope) {
@@ -116,17 +124,18 @@ export function GoalTable(props: GoalTableProps): JSX.Element {
     } else {
       model.setFilter();
     }
-    const goals = model.getRowCount();
-    const total = model.getTotalRowCount();
-    onFilter(goals, total);
-  }, [model, scope, failed, onFilter]);
+  }, [model, scope, failed]);
+
+  React.useEffect(() => setGoals(goals), [goals, setGoals]);
+  React.useEffect(() => setTotal(total), [total, setTotal]);
 
   return (
     <Table
       model={model}
+      display={display}
       settings='wp.goals'
-      onSelection={onWpoSelection}
-      selection={wpoSelection}
+      selection={current}
+      onSelection={onSelection}
     >
       <Column id='scope' label='Scope'
               width={150}

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

@@ -41,32 +41,46 @@ 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 [scoped, flipScoped] = Dome.useFlipSettings('frama-c.wp.goals.scoped',false);
+  const [failed, flipFailed] = Dome.useFlipSettings('frama-c.wp.goals.failed',true);
+  const [list, flipListView] = Dome.useFlipSettings('frama-c.wp.goals.list',true);
+  const [current, setCurrent] = React.useState(WP.goalDefault);
   const scope = States.useCurrentScope();
   const [goals, setGoals] = React.useState(0);
   const [total, setTotal] = React.useState(0);
-  const onFilter = React.useCallback((goals, total) => {
-    setGoals(goals);
-    setTotal(total);
-  }, [setGoals, setTotal]);
-  const current = scoped ? scope : undefined;
-    return (
-      <>
-        <Ivette.TitleBar>
-          <Label display={goals < total}>
-            {goals} / {total}
-          </Label>
-          <Inset />
-          <IconButton icon='COMPONENT' title='Current Scope Only'
-                      enabled={!!current}
-                      selected={scoped} onClick={flipScoped} />
-          <IconButton icon='CIRC.QUESTION' title='Unresolved Goals Only'
-                      selected={failed} onClick={flipFailed} />
-        </Ivette.TitleBar>
-        <GoalTable scope={scope} failed={failed} onFilter={onFilter} />
-      </>
-    );
+  const hasGoals = total > 0;
+  return (
+    <>
+      <Ivette.TitleBar>
+        <Label display={goals < total}>
+          {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='ITEMS.LIST'
+                    title='Goals List / Current Goal Details'
+                    enabled={hasGoals}
+                    selected={list}
+                    onClick={flipListView} />
+      </Ivette.TitleBar>
+      <GoalTable
+        display={list}
+        scope={scope}
+        failed={failed}
+        current={current}
+        setCurrent={setCurrent}
+        setGoals={setGoals}
+        setTotal={setTotal}
+      />
+    </>
+  );
 }
 
 Ivette.registerComponent({

ivette/src/frama-c/states.ts

@@ -409,6 +409,7 @@ export function reloadArray<K, A>(arr: Array<K, A>): void {
 
 /** Access to Synchronized Array elements. */
 export interface ArrayProxy<K, A> {
+  model: CompactModel<K,A>;
   length: number;
   getData(elt: K | undefined): (A | undefined);
   forEach(fn: (row: A, elt: K) => void): void;
@@ -429,6 +430,7 @@ function arrayProxy<K, A>(
   _stamp: number,
 ): ArrayProxy<K, A> {
   return {
+    model,
     length: model.length(),
     getData: (elt) => elt ? model.getData(elt) : undefined,
     forEach: (fn) => model.forEach((r) => fn(r, model.getkey(r))),