Skip to content
Snippets Groups Projects
Commit b3c2b095 authored by Michele Alberti's avatar Michele Alberti
Browse files

[ivette] Rename MultipleSelection into Locations.

parent 39b9be48
No related branches found
No related tags found
No related merge requests found
...@@ -684,7 +684,10 @@ const GlobalSelection = new GlobalStates.State<Selection>({ ...@@ -684,7 +684,10 @@ const GlobalSelection = new GlobalStates.State<Selection>({
prevSelections: [], prevSelections: [],
nextSelections: [], nextSelections: [],
}, },
multiple: { index: 0, allSelections: [] }, multiple: {
index: 0,
allSelections: [],
},
}); });
/** /**
......
...@@ -20,7 +20,7 @@ import ASTview from './ASTview'; ...@@ -20,7 +20,7 @@ import ASTview from './ASTview';
import ASTinfo from './ASTinfo'; import ASTinfo from './ASTinfo';
import Globals from './Globals'; import Globals from './Globals';
import Properties from './Properties'; import Properties from './Properties';
import MultipleSelection from './MultipleSelection'; import Locations from './Locations';
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
// --- Selection Controls // --- Selection Controls
...@@ -100,7 +100,7 @@ export default (() => { ...@@ -100,7 +100,7 @@ export default (() => {
<Properties /> <Properties />
<ASTview /> <ASTview />
<ASTinfo /> <ASTinfo />
<MultipleSelection /> <Locations />
</Group> </Group>
</LabView> </LabView>
</Splitter> </Splitter>
......
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
// --- Table of multiple selection // --- Table of (multiple) locations
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
import React from 'react'; import React from 'react';
...@@ -12,30 +12,30 @@ import * as Toolbar from 'dome/frame/toolbars'; ...@@ -12,30 +12,30 @@ import * as Toolbar from 'dome/frame/toolbars';
import { Component } from 'frama-c/LabViews'; import { Component } from 'frama-c/LabViews';
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
// --- Multiple Selection Panel // --- Locations Panel
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
type SelectionId = States.Location & { id: number }; type LocationId = States.Location & { id: number };
const SelectionTable = () => { const LocationsTable = () => {
// Hooks // Hooks
const [selection, updateSelection] = States.useSelection(); const [selection, updateSelection] = States.useSelection();
const model = React.useMemo(() => ( const model = React.useMemo(() => (
new CompactModel<number, SelectionId>(({ id }: SelectionId) => id) new CompactModel<number, LocationId>(({ id }: LocationId) => id)
), []); ), []);
const multiple: States.MultipleSelection = selection?.multiple; const multiple: States.MultipleSelection = selection?.multiple;
const numblerOfSelections = multiple?.allSelections?.length; const numberOfSelections = multiple?.allSelections?.length;
// Updates [[model]] with the current multiple selection. // Updates [[model]] with the current multiple selection.
React.useEffect(() => { React.useEffect(() => {
if (numblerOfSelections > 0) { if (numberOfSelections > 0) {
const data: SelectionId[] = const data: LocationId[] =
multiple.allSelections.map((d, i) => ({ ...d, id: i })); multiple.allSelections.map((d, i) => ({ ...d, id: i }));
model.replaceAllDataWith(data); model.replaceAllDataWith(data);
} else } else
model.clear(); model.clear();
}, [numblerOfSelections, multiple, model]); }, [numberOfSelections, multiple, model]);
// Callbacks // Callbacks
const onTableSelection = React.useCallback( const onTableSelection = React.useCallback(
...@@ -55,38 +55,38 @@ const SelectionTable = () => { ...@@ -55,38 +55,38 @@ const SelectionTable = () => {
<Toolbar.Button <Toolbar.Button
icon="RELOAD" icon="RELOAD"
onClick={reload} onClick={reload}
enabled={numblerOfSelections > 1} enabled={numberOfSelections > 1}
title="Reload the current location of the multiple selection" title="Reload the current location of the multiple selection"
/> />
<Toolbar.ButtonGroup> <Toolbar.ButtonGroup>
<Toolbar.Button <Toolbar.Button
icon="ANGLE.LEFT" icon="ANGLE.LEFT"
onClick={() => updateSelection('MULTIPLE_PREV')} onClick={() => updateSelection('MULTIPLE_PREV')}
enabled={numblerOfSelections > 1 && multiple?.index > 0} enabled={numberOfSelections > 1 && multiple?.index > 0}
title="Previous location of the multiple selection" title="Previous location of the multiple selection"
/> />
<Toolbar.Button <Toolbar.Button
icon="ANGLE.RIGHT" icon="ANGLE.RIGHT"
onClick={() => updateSelection('MULTIPLE_NEXT')} onClick={() => updateSelection('MULTIPLE_NEXT')}
enabled={ enabled={
numblerOfSelections > 1 && numberOfSelections > 1 &&
multiple?.index < numblerOfSelections - 1 multiple?.index < numberOfSelections - 1
} }
title="Next location of the multiple selection" title="Next location of the multiple selection"
/> />
</Toolbar.ButtonGroup> </Toolbar.ButtonGroup>
<Label <Label
className="component-info" className="component-info"
title={`${numblerOfSelections} selected locations`} title={`${numberOfSelections} selected locations`}
display={numblerOfSelections > 1} display={numberOfSelections > 1}
> >
{multiple?.index + 1} / {numblerOfSelections} {multiple?.index + 1} / {numberOfSelections}
</Label> </Label>
<Toolbar.Filler /> <Toolbar.Filler />
<Toolbar.Button <Toolbar.Button
icon="CIRC.CLOSE" icon="CIRC.CLOSE"
onClick={() => updateSelection('MULTIPLE_CLEAR')} onClick={() => updateSelection('MULTIPLE_CLEAR')}
enabled={numblerOfSelections > 1} enabled={numberOfSelections > 1}
title="Clear the multiple selection" title="Clear the multiple selection"
/> />
</Toolbar.ToolBar> </Toolbar.ToolBar>
...@@ -116,10 +116,10 @@ const SelectionTable = () => { ...@@ -116,10 +116,10 @@ const SelectionTable = () => {
export default () => ( export default () => (
<Component <Component
id="frama-c.selection" id="frama-c.selection"
label="Multiple Selection" label="Locations"
title="Browse a selection of multiple locations" title="Browse a selection of multiple locations"
> >
<SelectionTable /> <LocationsTable />
</Component> </Component>
); );
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment