Skip to content
Snippets Groups Projects
Commit 15671e74 authored by David Bühler's avatar David Bühler
Browse files

[ivette] Locations: prints the position and description of statements.

Instead of their id.
parent cfb2a3b3
No related branches found
No related tags found
No related merge requests found
...@@ -5,12 +5,14 @@ ...@@ -5,12 +5,14 @@
import React from 'react'; import React from 'react';
import * as States from 'frama-c/states'; import * as States from 'frama-c/states';
import * as Json from 'dome/data/json';
import { CompactModel } from 'dome/table/arrays'; import { CompactModel } from 'dome/table/arrays';
import { Table, Column } from 'dome/table/views'; import { Table, Column, Renderer } from 'dome/table/views';
import { Label } from 'dome/controls/labels'; import { Label } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons'; import { IconButton } from 'dome/controls/buttons';
import { Space } from 'dome/frame/toolbars'; import { Space } from 'dome/frame/toolbars';
import { Component, TitleBar } from 'frama-c/LabViews'; import { Component, TitleBar } from 'frama-c/LabViews';
import { markerInfo } from 'frama-c/api/kernel/ast';
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
// --- Locations Panel // --- Locations Panel
...@@ -27,6 +29,17 @@ const LocationsTable = () => { ...@@ -27,6 +29,17 @@ const LocationsTable = () => {
), []); ), []);
const multipleSelections = selection?.multiple; const multipleSelections = selection?.multiple;
const numberOfSelections = multipleSelections?.allSelections?.length; const numberOfSelections = multipleSelections?.allSelections?.length;
const markersInfo = States.useSyncArray(markerInfo);
// Renderer for statement markers.
const renderMarker: Renderer<string> =
(loc: string) => {
const markerId = (loc as Json.key<'#markerInfo'>);
const info = markersInfo.getData(markerId);
const source = info?.position;
const position = `${source?.base}:${source?.line}`;
return <Label label={position} title={info?.descr} />;
};
// Updates [[model]] with the current multiple selections. // Updates [[model]] with the current multiple selections.
React.useEffect(() => { React.useEffect(() => {
...@@ -112,7 +125,12 @@ const LocationsTable = () => { ...@@ -112,7 +125,12 @@ const LocationsTable = () => {
getter={(r: { id: number }) => r.id + 1} getter={(r: { id: number }) => r.id + 1}
/> />
<Column id="function" label="Function" width={120} /> <Column id="function" label="Function" width={120} />
<Column id="marker" label="Marker" fill /> <Column
id="marker"
label="Statement"
fill
render={renderMarker}
/>
</Table> </Table>
</> </>
); );
......
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