[ivette] Add first implementation of code navigation history in terms of location selections.

ivette/src/frama-c/states.ts

@@ -507,21 +507,112 @@ export function useSyncArray(id: string) {
 // --- Selection
 // --------------------------------------------------------------------------
 
+/** An AST location. */
+export interface Location {
+  /** Function name. */
+  readonly function: string;
+  /** Marker identifier. */
+  readonly marker?: string;
+}
+
+export interface Selection {
+  /** Current selection. */
+  current?: Location;
+  /** Previous locations with respect to the [[current]] one. */
+  prevSelections: Location[];
+  /** Next locations with respect to the [[current]] one. */
+  nextSelections: Location[];
+}
+
+/** An action on a location. */
+export interface LocationAction {
+  /** Type of action:
+   * - `SELECT` selects a given [[location]].
+   * - `GOTO` jumps to a given [[location]], and empties [[nextSelections]].
+   */
+  readonly type: 'SELECT' | 'GOTO';
+  readonly location: Location;
+}
+
+/** Actions on selection:
+ * - [[LocationAction]].
+ * - `GO_BACK` jumps to previous location (first in [[prevSelections]]).
+ * - `GO_FORWARD` jumps to next location (first in [[nextSelections]]).
+ */
+export type SelectionActions = LocationAction | 'GO_BACK' | 'GO_FORWARD';
+
+function isOnLocation(a: SelectionActions): a is LocationAction {
+  return (a as LocationAction).type !== undefined;
+}
+
+/** Compute the next selection based on the current one and the given action. */
+function reducer(s: Selection, action: SelectionActions) {
+  if (isOnLocation(action)) {
+    switch (action.type) {
+      case 'SELECT':
+        // Save current location if the selected one is in a different function.
+        if (s.current?.function !== action.location.function &&
+          (s.prevSelections.length !== 0 || s.nextSelections.length !== 0)) {
+          return {
+            current: action.location,
+            prevSelections: [s.current, ...s.prevSelections],
+            nextSelections: s.nextSelections,
+          };
+        }
+        return { ...s, current: action.location };
+      case 'GOTO':
+        return {
+          current: action.location,
+          prevSelections: [s.current, ...s.prevSelections],
+          nextSelections: [],
+        };
+      default:
+        return s;
+    }
+  } else {
+    const [pS, ...prevS] = s.prevSelections;
+    const [nS, ...nextS] = s.nextSelections;
+    switch (action) {
+      case 'GO_BACK':
+        return {
+          current: pS,
+          prevSelections: prevS,
+          nextSelections: [s.current, ...s.nextSelections],
+        };
+      case 'GO_FORWARD':
+        return {
+          current: nS,
+          prevSelections: [s.current, ...s.prevSelections],
+          nextSelections: nextS,
+        };
+      default:
+        return s;
+    }
+  }
+}
+
 const SELECTION = 'kernel.selection';
 
-setStateDefault(SELECTION, {});
+const initialSelection = {
+  current: undefined,
+  prevSelections: [],
+  nextSelections: [],
+};
+setStateDefault(SELECTION, initialSelection);
 
 /**
- *  @summary Current selection state.
- *  @return {array} `[selection,update]` for the current selection
- *  @description
- *  The selection is an object with many independant fields.
- *  You update it by providing only some fields, the other ones being kept
- *  unchanged, like the `setState()` behaviour of React components.
+ *  Current selection.
+ *  @return {array} The current selection and the function to update it.
  */
-export function useSelection() {
-  const [state, setState] = useState(SELECTION);
-  return [state, (upd: any) => setState({ ...state, ...upd })];
+export function useSelection(): [Selection, (a: SelectionActions) => void] {
+  const [selection, setSelection] = useState(SELECTION);
+
+  function update(action: SelectionActions) {
+    const nextSelection = reducer(selection, action);
+    setSelection(nextSelection);
+  }
+
+  return [selection, update];
 }
 
 // --------------------------------------------------------------------------

ivette/src/renderer/ASTinfo.tsx

@@ -17,8 +17,8 @@ import { Component } from 'frama-c/LabViews';
 const ASTinfo = () => {
 
   const buffer = React.useMemo(() => new RichTextBuffer(), []);
-  const [select, setSelect] = States.useSelection();
-  const marker = select && select.marker;
+  const [selection, updateSelection] = States.useSelection();
+  const marker = selection?.current?.marker;
   const data = States.useRequest(
     'kernel.ast.info',
     marker,
@@ -33,9 +33,10 @@ const ASTinfo = () => {
   }, [buffer, data]);
 
   // Callbacks
-  function onSelection(name: string) {
+  function onTextSelection(id: string) {
     // For now, the only markers are functions.
-    setSelect({ function: name, marker: undefined });
+    const location = { function: id };
+    updateSelection({ type: 'SELECT', location });
   }
 
   // Component
@@ -46,7 +47,7 @@ const ASTinfo = () => {
           buffer={buffer}
           mode="text"
           theme="default"
-          onSelection={onSelection}
+          onSelection={onTextSelection}
           readOnly
         />
       </Vfill>

ivette/src/renderer/ASTview.tsx

@@ -72,15 +72,15 @@ const ASTview = () => {
 
   // Hooks
   const buffer = React.useMemo(() => new RichTextBuffer(), []);
-  const printed = React.useRef();
-  const [select, setSelect] = States.useSelection();
+  const printed: React.MutableRefObject<string | undefined> = React.useRef();
+  const [selection, updateSelection] = States.useSelection();
   const [theme, setTheme] = Dome.useGlobalSetting('ASTview.theme', 'default');
   const [fontSize, setFontSize] = Dome.useGlobalSetting('ASTview.fontSize', 12);
   const [wrapText, setWrapText] = Dome.useSwitch('ASTview.wrapText', false);
   const markers = States.useSyncArray('kernel.ast.markerKind');
 
-  const theFunction = select && select.function;
-  const theMarker = select && select.marker;
+  const theFunction = selection?.current?.function;
+  const theMarker = selection?.current?.marker;
 
   // Hook: async loading
   React.useEffect(() => {
@@ -96,18 +96,30 @@ const ASTview = () => {
   }, [buffer, theMarker]);
 
   // Callbacks
+  const doPrevSelect = () => { updateSelection('GO_BACK'); };
+  const doNextSelect = () => { updateSelection('GO_FORWARD'); };
+
   const zoomIn = () => fontSize < 48 && setFontSize(fontSize + 2);
   const zoomOut = () => fontSize > 4 && setFontSize(fontSize - 2);
-  const onSelection = (marker: any) => setSelect({ marker });
 
-  function contextMenu(id: string) {
+  function onTextSelection(id: string) {
+    if (selection.current) {
+      const location = { ...selection.current, marker: id };
+      updateSelection({ type: 'SELECT', location });
+    }
+  }
+
+  function onContextMenu(id: string) {
     const marker = markers[id];
     if (marker && marker.kind === 'function') {
-      const item1 = {
+      const item = {
         label: `Go to definition of ${marker.name}`,
-        onClick: () => setSelect({ function: marker.name, marker: undefined }),
+        onClick: () => {
+          const location = { function: marker.name };
+          updateSelection({ type: 'GOTO', location });
+        },
       };
-      Dome.popupMenu([item1]);
+      Dome.popupMenu([item]);
     }
   }
 
@@ -122,6 +134,18 @@ const ASTview = () => {
   return (
     <>
       <TitleBar>
+        <IconButton
+          icon="MEDIA.PREV"
+          onClick={doPrevSelect}
+          disabled={!selection || selection.prevSelections.length === 0}
+          title="Previous location"
+        />
+        <IconButton
+          icon="MEDIA.NEXT"
+          onClick={doNextSelect}
+          disabled={!selection || selection.nextSelections.length === 0}
+          title="Next location"
+        />
         <IconButton
           icon="ZOOM.OUT"
           onClick={zoomOut}
@@ -153,8 +177,8 @@ const ASTview = () => {
         fontSize={fontSize}
         lineWrapping={wrapText}
         selection={theMarker}
-        onSelection={onSelection}
-        onContextMenu={contextMenu}
+        onSelection={onTextSelection}
+        onContextMenu={onContextMenu}
         readOnly
       />
     </>

ivette/src/renderer/Properties.tsx

@@ -87,17 +87,17 @@ class PropertyModel extends ArrayModel<Property> {
 const RenderTable = () => {
   // Hooks
   const model = React.useMemo(() => new PropertyModel(), []);
-  const items: { [key: string]: Property } =
+  const properties: { [key: string]: Property } =
     States.useSyncArray('kernel.properties');
   const statusDict: { [status: string]: Tag } =
     States.useDictionary('kernel.dictionary.propstatus');
-  const [select, setSelect] =
+  const [selection, updateSelection] =
     States.useSelection();
 
   React.useEffect(() => {
-    const data = _.toArray(items);
+    const data = _.toArray(properties);
     model.replace(data);
-  }, [model, items]);
+  }, [model, properties]);
 
   // Callbacks
   const getStatus = React.useCallback(
@@ -105,21 +105,24 @@ const RenderTable = () => {
     [statusDict],
   );
 
-  const onSelection = React.useCallback(
+  const onPropertySelection = React.useCallback(
     ({ key, function: fct }: Property) => {
-      setSelect({ marker: key, function: fct });
-    }, [setSelect],
+      if (fct) {
+        const location = { function: fct, marker: key };
+        updateSelection({ type: 'SELECT', location });
+      }
+    }, [updateSelection],
   );
 
-  const selection = select?.marker;
+  const propertySelection = selection?.current?.marker;
 
   // Rendering
   return (
     <Table<string, Property>
       model={model}
       sorting={model}
-      selection={selection}
-      onSelection={onSelection}
+      selection={propertySelection}
+      onSelection={onPropertySelection}
       settings="ivette.properties.table"
     >
       <ColumnCode id="function" label="Function" width={120} />