diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index e0515681e67ad61d75bc699cc26c539f0f19abc6..0ed83e5c84573094db290629aba27b66218373cb 100644
--- a/ivette/src/frama-c/states.ts
+++ b/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];
}
// --------------------------------------------------------------------------
diff --git a/ivette/src/renderer/ASTinfo.tsx b/ivette/src/renderer/ASTinfo.tsx
index ec3106bddd7692a622ffa3f7c210f21acb0cb012..b2b1c16d21860e3160ef5c65e695c4e7328d096d 100644
--- a/ivette/src/renderer/ASTinfo.tsx
+++ b/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>
diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx
index 4b85a415ae25464c08740c887589bd6d11158ce5..75506913f91ffd69cccd7b1680298b2a38a11444 100644
--- a/ivette/src/renderer/ASTview.tsx
+++ b/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
/>
</>
diff --git a/ivette/src/renderer/Properties.tsx b/ivette/src/renderer/Properties.tsx
index 3061204a39bbad89fbd9a1b5213c57263769514e..ed54c3d6d59163e27f9df6d526bd4264b884087b 100644
--- a/ivette/src/renderer/Properties.tsx
+++ b/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} />