[ivette] Some refactoring of the multiple selection state.

ivette/src/frama-c/states.ts

@@ -507,7 +507,8 @@ export function useSyncArray(id: string) {
 // --- Selection
 // --------------------------------------------------------------------------
 
-type AtLeastOne<T, U = {[K in keyof T]: Pick<T, K> }> = Partial<T> & U[keyof U];
+type AtLeastOne<T, U = { [K in keyof T]: Pick<T, K> }> =
+  Partial<T> & U[keyof U];
 
 export interface FullLocation {
   /** Function name. */
@@ -523,112 +524,204 @@ export interface FullLocation {
  */
 export type Location = AtLeastOne<FullLocation>;
 
-export interface Selection {
-  /** Current selection. */
-  current?: Location;
+export interface HistorySelection {
   /** Previous locations with respect to the [[current]] one. */
   prevSelections: Location[];
   /** Next locations with respect to the [[current]] one. */
   nextSelections: Location[];
-  /** Selection of multiple locations at once. Can be cycled through
-      'NEXT' and 'PREV' actions. */
-  multiple: Location[];
-  /** The index of the last selected location from [[multiple]]. */
-  index: number;
 }
 
-/** A select action on a location. */
-export interface SelectAction {
-  readonly location: Location;
+/** Actions on history selections:
+ * - `HISTORY_PREV` jumps to previous history location
+ *   (first in [[prevSelections]]).
+ * - `HISTORY_NEXT` jumps to next history location
+ *   (first in [[nextSelections]]).
+ */
+type HistorySelectActions = 'HISTORY_PREV' | 'HISTORY_NEXT';
+
+/** A selection of multiple locations. */
+export interface MultipleSelection {
+  /** The index of the current selected location in [[possibleSelections]]. */
+  index: number;
+  /** All locations forming a multiple selection. */
+  allSelections: Location[];
 }
 
-/** A select action on an array of location. */
-export interface SelectArrayAction {
+/** A select action on multiple locations. */
+export interface MultipleSelect {
   readonly locations: Location[];
 }
 
 /** Select the [[index]]-nth location of the current multiple selection. */
-export interface GotoAction {
+export interface NthSelect {
   readonly index: number;
 }
 
+/** Actions on multiple selections:
+ * - [[MultipleSelect]].
+ * - [[NthSelect]].
+ * - `MULTIPLE_PREV` jumps to previous location of the multiple selections.
+ * - `MULTIPLE_NEXT` jumps to next location of the multiple selections.
+ */
+type MultipleSelectActions =
+  MultipleSelect | NthSelect
+  | 'MULTIPLE_PREV' | 'MULTIPLE_NEXT' | 'MULTIPLE_CLEAR';
+
+
+export interface Selection {
+  /** Current selection. May be one in [[history]] or [[multiple]]. */
+  current?: Location;
+  /** History of selections. */
+  history: HistorySelection;
+  /** Multiple selections at once. */
+  multiple: MultipleSelection;
+}
+
+/** A select action on a location. */
+export interface SingleSelect {
+  readonly location: Location;
+}
+
 /** Actions on selection:
- * - [[SelectAction]].
- * - `GO_BACK` jumps to previous location (first in [[prevSelections]]).
- * - `GO_FORWARD` jumps to next location (first in [[nextSelections]]).
+ * - [[SingleSelect]].
+ * - [[HistorySelectActions]].
+ * - [[MultipleSelectActions]].
  */
 export type SelectionActions =
-  SelectAction | SelectArrayAction | GotoAction
-  | 'GO_BACK' | 'GO_FORWARD' | 'NEXT' | 'PREV' | 'CLEAR';
+  SingleSelect | HistorySelectActions | MultipleSelectActions;
 
-function isSelect(a: SelectionActions): a is SelectAction {
-  return (a as SelectAction).location !== undefined;
+function isSingleSelect(a: SelectionActions): a is SingleSelect {
+  return (a as SingleSelect).location !== undefined;
 }
 
-function isSelectArray(a: SelectionActions): a is SelectArrayAction {
-  return (a as SelectArrayAction).locations !== undefined;
+function isMultipleSelect(a: SelectionActions): a is MultipleSelect {
+  return (a as MultipleSelect).locations !== undefined;
 }
 
-function isGoto(a: SelectionActions): a is GotoAction {
-  return (a as GotoAction).index !== undefined;
+function isNthSelect(a: SelectionActions): a is NthSelect {
+  return (a as NthSelect).index !== undefined;
 }
 
-function select(s: Selection, location: Location): Selection {
+/** Update selection to the given location. */
+function selectLocation(s: Selection, location: Location): Selection {
   const [prevSelections, nextSelections] =
     s.current && s.current.function !== location.function ?
-      [[s.current, ...s.prevSelections], []] :
-      [s.prevSelections, s.nextSelections];
-  return { ...s, current: location, prevSelections, nextSelections };
+      [[s.current, ...s.history.prevSelections], []] :
+      [s.history.prevSelections, s.history.nextSelections];
+  return {
+    ...s,
+    current: location,
+    history: { prevSelections, nextSelections },
+  };
+}
+
+/** Compute the next selection picking from the current history, depending on
+ *  action.
+ */
+function fromHistory(s: Selection, action: HistorySelectActions): Selection {
+  switch (action) {
+    case 'HISTORY_PREV': {
+      const [pS, ...prevS] = s.history.prevSelections;
+      return {
+        ...s,
+        current: pS,
+        history: {
+          prevSelections: prevS,
+          nextSelections:
+            [(s.current as Location), ...s.history.nextSelections],
+        },
+      };
+    }
+    case 'HISTORY_NEXT': {
+      const [nS, ...nextS] = s.history.nextSelections;
+      return {
+        ...s,
+        current: nS,
+        history: {
+          prevSelections:
+            [(s.current as Location), ...s.history.prevSelections],
+          nextSelections: nextS,
+        },
+      };
+    }
+    default:
+      return s;
+  }
+}
+
+/** Compute the next selection picking from the current multiple, depending on
+ *  action.
+ */
+function fromMultipleSelections(
+  s: Selection,
+  action: 'MULTIPLE_PREV' | 'MULTIPLE_NEXT' | 'MULTIPLE_CLEAR',
+): Selection {
+  switch (action) {
+    case 'MULTIPLE_PREV':
+    case 'MULTIPLE_NEXT': {
+      const index =
+        action === 'MULTIPLE_NEXT' ?
+          s.multiple.index + 1 :
+          s.multiple.index - 1;
+      if (0 <= index && index < s.multiple.allSelections.length) {
+        const multiple = { ...s.multiple, index };
+        return selectLocation(
+          { ...s, multiple },
+          s.multiple.allSelections[index],
+        );
+      }
+      return s;
+    }
+    case 'MULTIPLE_CLEAR':
+      return {
+        ...s,
+        multiple: {
+          index: 0,
+          allSelections: [],
+        },
+      };
+    default:
+      return s;
+  }
 }
 
 /** Compute the next selection based on the current one and the given action. */
 function reducer(s: Selection, action: SelectionActions): Selection {
-  if (isSelect(action)) {
-    return select(s, action.location);
+  if (isSingleSelect(action)) {
+    return selectLocation(s, action.location);
   }
-  if (isSelectArray(action)) {
+  if (isMultipleSelect(action)) {
     if (action.locations.length === 0)
       return s;
+    const selection = selectLocation(s, action.locations[0]);
     if (action.locations.length === 1)
-      return select(s, action.locations[0]);
-    const selection = select(s, action.locations[0]);
-    return { ...selection, multiple: action.locations, index: 0 };
-
+      return selection;
+    return {
+      ...selection,
+      multiple: {
+        allSelections: action.locations,
+        index: 0,
+      },
+    };
   }
-  if (isGoto(action)) {
+  if (isNthSelect(action)) {
     const { index } = action;
-    if (0 <= index && index < s.multiple.length) {
-      const location = s?.multiple[index];
-      const selection = select(s, location);
-      return { ...selection, index: action.index };
+    if (0 <= index && index < s.multiple.allSelections.length) {
+      const location = s?.multiple.allSelections[index];
+      const selection = selectLocation(s, location);
+      const multiple = { ...selection.multiple, index };
+      return { ...selection, multiple };
     }
     return s;
   }
-  const [pS, ...prevS] = s.prevSelections;
-  const [nS, ...nextS] = s.nextSelections;
-  const index = action === 'NEXT' ? s.index + 1 : s.index - 1;
   switch (action) {
-    case 'GO_BACK':
-      return {
-        ...s,
-        current: pS,
-        prevSelections: prevS,
-        nextSelections: [(s.current as Location), ...s.nextSelections],
-      };
-    case 'GO_FORWARD':
-      return {
-        ...s,
-        current: nS,
-        prevSelections: [(s.current as Location), ...s.prevSelections],
-        nextSelections: nextS,
-      };
-    case 'NEXT':
-    case 'PREV':
-      if (0 <= index && index < s.multiple.length)
-        return select({ ...s, index }, s.multiple[index]);
-      return s;
-    case 'CLEAR':
-      return { ...s, multiple: [], index: 0 };
+    case 'HISTORY_PREV':
+    case 'HISTORY_NEXT':
+      return fromHistory(s, action);
+    case 'MULTIPLE_PREV':
+    case 'MULTIPLE_NEXT':
+    case 'MULTIPLE_CLEAR':
+      return fromMultipleSelections(s, action);
     default:
       return s;
   }
@@ -638,8 +731,10 @@ const SELECTION = 'kernel.selection';
 
 const initialSelection = {
   current: undefined,
-  prevSelections: [],
-  nextSelections: [],
+  history: {
+    prevSelections: [],
+    nextSelections: [],
+  },
   multiple: [],
   index: 0,
 };

ivette/src/renderer/ASTview.tsx

@@ -64,7 +64,10 @@ async function loadAST(
   }
 }
 
-async function callers(updateSelection: any, kf: string) {
+async function functionCallers(
+  updateSelection: (a: States.SelectionActions) => void,
+  kf: string,
+) {
   try {
     const data = await Server.GET({
       endpoint: 'eva.callers',
@@ -75,7 +78,7 @@ async function callers(updateSelection: any, kf: string) {
     ));
     updateSelection({ locations });
   } catch (err) {
-    PP.error('Fail to retrieve callers of function', kf, err);
+    PP.error(`Fail to retrieve callers of function ${kf}`, err);
   }
 }
 
@@ -89,7 +92,7 @@ const ASTview = () => {
   const buffer = React.useMemo(() => new RichTextBuffer(), []);
   const printed: React.MutableRefObject<string | undefined> = React.useRef();
   const [selection, updateSelection] = States.useSelection();
-  const multiple = selection?.multiple;
+  const multipleSelections = selection?.multiple.allSelections;
   const [theme, setTheme] = Dome.useGlobalSetting('ASTview.theme', 'default');
   const [fontSize, setFontSize] = Dome.useGlobalSetting('ASTview.fontSize', 12);
   const [wrapText, setWrapText] = Dome.useSwitch('ASTview.wrapText', false);
@@ -108,12 +111,12 @@ const ASTview = () => {
 
   React.useEffect(() => {
     const decorator = (marker: string) => {
-      if (multiple.some((location) => location?.marker === marker))
+      if (multipleSelections?.some((location) => location?.marker === marker))
         return 'highlighted-marker';
       return undefined;
     };
     buffer.setDecorator(decorator);
-  }, [buffer, multiple]);
+  }, [buffer, multipleSelections]);
 
   // Hook: marker scrolling
   React.useEffect(() => {
@@ -144,11 +147,11 @@ const ASTview = () => {
       });
     }
     if (marker?.kind === 'declaration'
-        && marker?.var === 'function'
-        && marker?.name) {
+      && marker?.var === 'function'
+      && marker?.name) {
       items.push({
         label: 'Go to callers',
-        onClick: () => callers(updateSelection, marker.name),
+        onClick: () => functionCallers(updateSelection, marker.name),
       });
     }
     if (items.length > 0)

ivette/src/renderer/Application.tsx

@@ -26,24 +26,24 @@ import MultipleSelection from './MultipleSelection';
 // --- Selection Controls
 // --------------------------------------------------------------------------
 
-const SelectionControls = () => {
+const HistorySelectionControls = () => {
   const [selection, updateSelection] = States.useSelection();
 
-  const doPrevSelect = () => { updateSelection('GO_BACK'); };
-  const doNextSelect = () => { updateSelection('GO_FORWARD'); };
+  const doPrevSelect = () => { updateSelection('HISTORY_PREV'); };
+  const doNextSelect = () => { updateSelection('HISTORY_NEXT'); };
 
   return (
     <Toolbar.ButtonGroup>
       <Toolbar.Button
         icon="MEDIA.PREV"
         onClick={doPrevSelect}
-        disabled={!selection || selection.prevSelections.length === 0}
+        disabled={!selection || selection.history.prevSelections.length === 0}
         title="Previous location"
       />
       <Toolbar.Button
         icon="MEDIA.NEXT"
         onClick={doNextSelect}
-        disabled={!selection || selection.nextSelections.length === 0}
+        disabled={!selection || selection.history.nextSelections.length === 0}
         title="Next location"
       />
     </Toolbar.ButtonGroup>
@@ -74,7 +74,7 @@ export default (() => {
           onClick={flipSidebar}
         />
         <Controller.Control />
-        <SelectionControls />
+        <HistorySelectionControls />
         <Toolbar.Filler />
         <Toolbar.Button
           icon="ITEMS.GRID"

ivette/src/renderer/MultipleSelection.tsx

@@ -19,18 +19,19 @@ const SelectionTable = () => {
 
   // Hooks
   const [selection, updateSelection] = States.useSelection();
-  const length = selection?.multiple?.length;
-  const multiple: States.Location[] = selection?.multiple;
   const model = React.useMemo(() => new ArrayModel('id'), []);
 
+  const multiple = selection?.multiple;
+  const numblerOfSelections = multiple?.allSelections?.length;
+
   // Updates [[model]] with the current multiple selection.
   React.useEffect(() => {
-    if (multiple?.length > 0) {
-      const array = multiple.map((d, i) => ({ ...d, id: i }));
+    if (numblerOfSelections > 0) {
+      const array = multiple.allSelections.map((d, i) => ({ ...d, id: i }));
       model.replace(array);
     } else
       model.clear();
-  }, [multiple, model]);
+  }, [numblerOfSelections, multiple, model]);
 
   // Callbacks
   const onTableSelection = React.useCallback(
@@ -39,7 +40,7 @@ const SelectionTable = () => {
   );
 
   const reload = () => {
-    const location = multiple[selection?.index];
+    const location = multiple.allSelections[multiple.index];
     updateSelection({ location });
   };
 
@@ -50,41 +51,44 @@ const SelectionTable = () => {
         <Toolbar.Button
           icon="RELOAD"
           onClick={reload}
-          enabled={length > 1}
+          enabled={numblerOfSelections > 1}
           title="Reload the current location of the multiple selection"
         />
         <Toolbar.ButtonGroup>
           <Toolbar.Button
             icon="ANGLE.LEFT"
-            onClick={() => updateSelection('PREV')}
-            enabled={length > 1 && selection?.index > 0}
+            onClick={() => updateSelection('MULTIPLE_PREV')}
+            enabled={numblerOfSelections > 1 && multiple?.index > 0}
             title="Previous location of the multiple selection"
           />
           <Toolbar.Button
             icon="ANGLE.RIGHT"
-            onClick={() => updateSelection('NEXT')}
-            enabled={length > 1 && selection?.index < length - 1}
+            onClick={() => updateSelection('MULTIPLE_NEXT')}
+            enabled={
+              numblerOfSelections > 1 &&
+              multiple?.index < numblerOfSelections - 1
+            }
             title="Next location of the multiple selection"
           />
         </Toolbar.ButtonGroup>
         <Label
           className="component-info"
-          title={`${length} selected locations`}
-          display={length > 1}
+          title={`${numblerOfSelections} selected locations`}
+          display={numblerOfSelections > 1}
         >
-          {selection?.index + 1} / {length}
+          {multiple?.index + 1} / {numblerOfSelections}
         </Label>
         <Toolbar.Filler />
         <Toolbar.Button
           icon="CIRC.CLOSE"
-          onClick={() => updateSelection('CLEAR')}
-          enabled={length > 1}
+          onClick={() => updateSelection('MULTIPLE_CLEAR')}
+          enabled={numblerOfSelections > 1}
           title="Clear the multiple selection"
         />
       </Toolbar.ToolBar>
       <Table
         model={model}
-        selection={selection?.index}
+        selection={multiple?.index}
         onSelection={onTableSelection}
       >
         <Column
@@ -92,7 +96,7 @@ const SelectionTable = () => {
           label="#"
           align="center"
           width={25}
-          getter={(r: {id: number}) => r.id + 1}
+          getter={(r: { id: number }) => r.id + 1}
         />
         <Column id="function" label="Function" width={120} />
         <Column id="marker" label="Marker" fill />