Skip to content
Snippets Groups Projects
Commit e9f1b491 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[ivette] display filtered properties ratio

parent b6c0966d
No related branches found
No related tags found
No related merge requests found
...@@ -73,6 +73,10 @@ export class MapModel<Key, Row> ...@@ -73,6 +73,10 @@ export class MapModel<Key, Row>
// Hold filtered & sorted data (computed on demand) // Hold filtered & sorted data (computed on demand)
private table?: TABLE<Key, Row>; private table?: TABLE<Key, Row>;
// Filtered-out Row Count
private filtered: number = 0;
// Filtering function // Filtering function
private filter?: Filter<Key, Row>; private filter?: Filter<Key, Row>;
...@@ -103,6 +107,7 @@ export class MapModel<Key, Row> ...@@ -103,6 +107,7 @@ export class MapModel<Key, Row>
// Lazily compute table // Lazily compute table
protected rebuild(): TABLE<Key, Row> { protected rebuild(): TABLE<Key, Row> {
const current = this.table; const current = this.table;
let filtered = 0;
if (current !== undefined) return current; if (current !== undefined) return current;
let table: TABLE<Key, Row> = []; let table: TABLE<Key, Row> = [];
try { try {
...@@ -111,6 +116,8 @@ export class MapModel<Key, Row> ...@@ -111,6 +116,8 @@ export class MapModel<Key, Row>
const phi = this.filter; const phi = this.filter;
if (!phi || phi(packed.row, packed.key)) if (!phi || phi(packed.row, packed.key))
table.push(packed); table.push(packed);
else
filtered++;
}); });
table.sort(this.sorter()); table.sort(this.sorter());
} catch (err) { } catch (err) {
...@@ -118,6 +125,7 @@ export class MapModel<Key, Row> ...@@ -118,6 +125,7 @@ export class MapModel<Key, Row>
} }
table.forEach((pack, index) => pack.index = index); table.forEach((pack, index) => pack.index = index);
this.table = table; this.table = table;
this.filtered = filtered;
return table; return table;
} }
...@@ -125,6 +133,9 @@ export class MapModel<Key, Row> ...@@ -125,6 +133,9 @@ export class MapModel<Key, Row>
// --- Proxy // --- Proxy
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
/** Non filtered. */
getTotalRowCount() { return this.getRowCount() + this.filtered; }
getRowCount() { return this.rebuild().length; } getRowCount() { return this.rebuild().length; }
getRowAt(k: number) { return this.rebuild()[k]?.row; } getRowAt(k: number) { return this.rebuild()[k]?.row; }
......
...@@ -277,7 +277,7 @@ const RenderConsole = () => { ...@@ -277,7 +277,7 @@ const RenderConsole = () => {
/> />
<Space /> <Space />
<Label <Label
className="controller-rank" className="component-info"
title="History (last command first)" title="History (last command first)"
display={edited} display={edited}
> >
......
...@@ -400,7 +400,8 @@ const PropertyColumns = () => { ...@@ -400,7 +400,8 @@ const PropertyColumns = () => {
<ColumnTag <ColumnTag
id="status" id="status"
label="Status" label="Status"
fixed width={100} fixed
width={100}
align="center" align="center"
getter={getStatus} getter={getStatus}
/> />
...@@ -409,6 +410,26 @@ const PropertyColumns = () => { ...@@ -409,6 +410,26 @@ const PropertyColumns = () => {
}; };
function FilterRatio({ model }: { model: PropertyModel }) {
const forceUpdate = Dome.useForceUpdate() as (() => void);
React.useEffect(() => {
const client = model.link();
client.onReload(forceUpdate);
return client.unlink;
});
const filtered = model.getRowCount();
const total = model.getTotalRowCount();
return (
<Label
className="component-info"
title="Displayed Properties / Total"
display={filtered !== total}
>
{filtered} / {total}
</Label>
);
}
// ------------------------------------------------------------------------- // -------------------------------------------------------------------------
// --- Properties Table // --- Properties Table
// ------------------------------------------------------------------------- // -------------------------------------------------------------------------
...@@ -432,7 +453,7 @@ const RenderTable = () => { ...@@ -432,7 +453,7 @@ const RenderTable = () => {
const selectedFunction = select?.function; const selectedFunction = select?.function;
React.useEffect(() => { React.useEffect(() => {
model.setFilterFunction(selectedFunction); model.setFilterFunction(selectedFunction);
}, [selectedFunction]); }, [model, selectedFunction]);
// Callbacks // Callbacks
const onSelection = React.useCallback( const onSelection = React.useCallback(
...@@ -446,7 +467,12 @@ const RenderTable = () => { ...@@ -446,7 +467,12 @@ const RenderTable = () => {
return ( return (
<> <>
<TitleBar> <TitleBar>
<IconButton icon='ITEMS.LIST' selected={showFilter} onClick={flipFilter} /> <FilterRatio model={model} />
<IconButton
icon="ITEMS.LIST"
selected={showFilter}
onClick={flipFilter}
/>
</TitleBar> </TitleBar>
<Splitter dir="RIGHT" unfold={showFilter}> <Splitter dir="RIGHT" unfold={showFilter}>
<Table<string, Property> <Table<string, Property>
......
...@@ -2,9 +2,11 @@ ...@@ -2,9 +2,11 @@
/* --- Frama-C Styling --- */ /* --- Frama-C Styling --- */
/* -------------------------------------------------------------------------- */ /* -------------------------------------------------------------------------- */
.controller-rank { .component-info {
color: #888 ; color: #888;
min-width: 50px; min-width: 50px;
padding-top: 4px;
font-size: smaller;
} }
.code-column { .code-column {
......
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