diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index e0515681e67ad61d75bc699cc26c539f0f19abc6..b33dd2204deded981a7c97496a0d21f697ccc76b 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -507,21 +507,102 @@ export function useSyncArray(id: string) {
// --- Selection
// --------------------------------------------------------------------------
+type AtLeastOne<T, U = {[K in keyof T]: Pick<T, K> }> = Partial<T> & U[keyof U];
+
+export interface FullLocation {
+ /** Function name. */
+ readonly function: string;
+ /** Marker identifier. */
+ readonly marker: string;
+}
+
+/** An AST location.
+ *
+ * Properties [[function]] and [[marker]] are optional,
+ * but at least one of the two must be set.
+ */
+export type Location = AtLeastOne<FullLocation>;
+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[];
+}
+
+/** A select action on a location. */
+export interface SelectAction {
+ 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]]).
+ */
+export type SelectionActions = SelectAction | 'GO_BACK' | 'GO_FORWARD';
+
+function isSelect(a: SelectionActions): a is SelectAction {
+ return (a as SelectAction).location !== undefined;
+}
+
+/** Compute the next selection based on the current one and the given action. */
+function reducer(s: Selection, action: SelectionActions): Selection {
+ if (isSelect(action)) {
+ const [prevSelections, nextSelections] =
+ s.current && s.current.function !== action.location.function ?
+ [[s.current, ...s.prevSelections], []] :
+ [s.prevSelections, s.nextSelections];
+ return {
+ current: action.location,
+ prevSelections,
+ nextSelections,
+ };
+ }
+ const [pS, ...prevS] = s.prevSelections;
+ const [nS, ...nextS] = s.nextSelections;
+ switch (action) {
+ case 'GO_BACK':
+ return {
+ current: pS,
+ prevSelections: prevS,
+ nextSelections: [(s.current as Location), ...s.nextSelections],
+ };
+ case 'GO_FORWARD':
+ return {
+ current: nS,
+ prevSelections: [(s.current as Location), ...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..6f3fb2bdca78057b36a6cc80b34e8c2c39af5343 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({ 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..b383770585a19e2eef98f8beba4d58850cf84a03 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(() => {
@@ -98,21 +98,30 @@ const ASTview = () => {
// Callbacks
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({ 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({ location });
+ },
};
- Dome.popupMenu([item1]);
+ Dome.popupMenu([item]);
}
}
// Theme Popup
- const selectTheme = (id?: string) => id && setTheme(id);
+ const selectTheme = (id: string) => setTheme(id);
const checkTheme =
(th: { id: string }) => ({ checked: th.id === theme, ...th });
const themePopup =
@@ -153,8 +162,8 @@ const ASTview = () => {
fontSize={fontSize}
lineWrapping={wrapText}
selection={theMarker}
- onSelection={onSelection}
- onContextMenu={contextMenu}
+ onSelection={onTextSelection}
+ onContextMenu={onContextMenu}
readOnly
/>
</>
diff --git a/ivette/src/renderer/Application.tsx b/ivette/src/renderer/Application.tsx
index e3c343f52bd17df20d95344b3d7e8594ec368b8f..16b901ab603d95f3cb156ce79304360966118e4b 100644
--- a/ivette/src/renderer/Application.tsx
+++ b/ivette/src/renderer/Application.tsx
@@ -4,6 +4,7 @@
import React from 'react';
import * as Dome from 'dome';
+import * as States from 'frama-c/states';
import { Vfill } from 'dome/layout/boxes';
import { Splitter } from 'dome/layout/splitters';
import * as Toolbar from 'dome/frame/toolbars';
@@ -18,6 +19,34 @@ import Properties from './Properties';
import ASTview from './ASTview';
import ASTinfo from './ASTinfo';
+// --------------------------------------------------------------------------
+// --- Selection Controls
+// --------------------------------------------------------------------------
+
+const SelectionControls = () => {
+ const [selection, updateSelection] = States.useSelection();
+
+ const doPrevSelect = () => { updateSelection('GO_BACK'); };
+ const doNextSelect = () => { updateSelection('GO_FORWARD'); };
+
+ return (
+ <Toolbar.ButtonGroup>
+ <Toolbar.Button
+ icon="MEDIA.PREV"
+ onClick={doPrevSelect}
+ disabled={!selection || selection.prevSelections.length === 0}
+ title="Previous location"
+ />
+ <Toolbar.Button
+ icon="MEDIA.NEXT"
+ onClick={doNextSelect}
+ disabled={!selection || selection.nextSelections.length === 0}
+ title="Next location"
+ />
+ </Toolbar.ButtonGroup>
+ );
+};
+
// --------------------------------------------------------------------------
// --- Main View
// --------------------------------------------------------------------------
@@ -42,6 +71,7 @@ export default (() => {
onClick={flipSidebar}
/>
<Controller.Control />
+ <SelectionControls />
<Toolbar.Filler />
<Toolbar.Button
icon="ITEMS.GRID"
diff --git a/ivette/src/renderer/Properties.tsx b/ivette/src/renderer/Properties.tsx
index ba8df8eb394f87319bfbd8ccbfc727f88af19e75..bd222dda4d7eac52c268d6e38973c4d0798b2257 100644
--- a/ivette/src/renderer/Properties.tsx
+++ b/ivette/src/renderer/Properties.tsx
@@ -437,32 +437,37 @@ function FilterRatio({ model }: { model: PropertyModel }) {
const RenderTable = () => {
// Hooks
const model = React.useMemo(() => new PropertyModel(), []);
- const items: { [key: string]: Property } =
+ const properties: { [key: string]: Property } =
States.useSyncArray('kernel.properties');
- const [select, setSelect] = States.useSelection();
+
+ const [selection, updateSelection] = States.useSelection();
+
const [showFilter, flipFilter] =
Dome.useSwitch('ivette.properties.showFilter', true);
// Populating the model
React.useEffect(() => {
- const data = _.toArray(items);
+ const data = _.toArray(properties);
model.replace(data);
- }, [model, items]);
+ }, [model, properties]);
// Updating the filter
- const selectedFunction = select?.function;
+ const selectedFunction = selection?.current?.function;
React.useEffect(() => {
model.setFilterFunction(selectedFunction);
}, [model, selectedFunction]);
+
// Callbacks
- const onSelection = React.useCallback(
+
+ const onPropertySelection = React.useCallback(
({ key, function: fct }: Property) => {
- setSelect({ marker: key, function: fct });
- }, [setSelect],
+ const location = { function: fct, marker: key };
+ updateSelection({ location });
+ }, [updateSelection],
);
- const selection = select?.marker;
+ const propertySelection = selection?.current?.marker;
return (
<>
@@ -478,8 +483,8 @@ const RenderTable = () => {
<Table<string, Property>
model={model}
sorting={model}
- selection={selection}
- onSelection={onSelection}
+ selection={propertySelection}
+ onSelection={onPropertySelection}
settings="ivette.properties.table"
>
<PropertyColumns />