From e9f1b49137ef3e8f93f574655075f0a587a9a05b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 9 Jun 2020 16:01:18 +0200
Subject: [PATCH] [ivette] display filtered properties ratio

---
 ivette/src/dome/src/renderer/table/arrays.ts | 11 +++++++
 ivette/src/renderer/Controller.tsx           |  2 +-
 ivette/src/renderer/Properties.tsx           | 32 ++++++++++++++++++--
 ivette/src/renderer/style.css                |  6 ++--
 4 files changed, 45 insertions(+), 6 deletions(-)

diff --git a/ivette/src/dome/src/renderer/table/arrays.ts b/ivette/src/dome/src/renderer/table/arrays.ts
index 9cdd951fea2..a0bdcca0db5 100644
--- a/ivette/src/dome/src/renderer/table/arrays.ts
+++ b/ivette/src/dome/src/renderer/table/arrays.ts
@@ -73,6 +73,10 @@ export class MapModel<Key, Row>
   // Hold filtered & sorted data (computed on demand)
   private table?: TABLE<Key, Row>;
 
+  // Filtered-out Row Count
+  private filtered: number = 0;
+
+
   // Filtering function
   private filter?: Filter<Key, Row>;
 
@@ -103,6 +107,7 @@ export class MapModel<Key, Row>
   // Lazily compute table
   protected rebuild(): TABLE<Key, Row> {
     const current = this.table;
+    let filtered = 0;
     if (current !== undefined) return current;
     let table: TABLE<Key, Row> = [];
     try {
@@ -111,6 +116,8 @@ export class MapModel<Key, Row>
         const phi = this.filter;
         if (!phi || phi(packed.row, packed.key))
           table.push(packed);
+        else
+          filtered++;
       });
       table.sort(this.sorter());
     } catch (err) {
@@ -118,6 +125,7 @@ export class MapModel<Key, Row>
     }
     table.forEach((pack, index) => pack.index = index);
     this.table = table;
+    this.filtered = filtered;
     return table;
   }
 
@@ -125,6 +133,9 @@ export class MapModel<Key, Row>
   // --- Proxy
   // --------------------------------------------------------------------------
 
+  /** Non filtered. */
+  getTotalRowCount() { return this.getRowCount() + this.filtered; }
+
   getRowCount() { return this.rebuild().length; }
 
   getRowAt(k: number) { return this.rebuild()[k]?.row; }
diff --git a/ivette/src/renderer/Controller.tsx b/ivette/src/renderer/Controller.tsx
index f14fdadc91f..01d73e3cb14 100644
--- a/ivette/src/renderer/Controller.tsx
+++ b/ivette/src/renderer/Controller.tsx
@@ -277,7 +277,7 @@ const RenderConsole = () => {
         />
         <Space />
         <Label
-          className="controller-rank"
+          className="component-info"
           title="History (last command first)"
           display={edited}
         >
diff --git a/ivette/src/renderer/Properties.tsx b/ivette/src/renderer/Properties.tsx
index 8f0a7e57db8..b4300001831 100644
--- a/ivette/src/renderer/Properties.tsx
+++ b/ivette/src/renderer/Properties.tsx
@@ -400,7 +400,8 @@ const PropertyColumns = () => {
       <ColumnTag
         id="status"
         label="Status"
-        fixed width={100}
+        fixed
+        width={100}
         align="center"
         getter={getStatus}
       />
@@ -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
 // -------------------------------------------------------------------------
@@ -432,7 +453,7 @@ const RenderTable = () => {
   const selectedFunction = select?.function;
   React.useEffect(() => {
     model.setFilterFunction(selectedFunction);
-  }, [selectedFunction]);
+  }, [model, selectedFunction]);
 
   // Callbacks
   const onSelection = React.useCallback(
@@ -446,7 +467,12 @@ const RenderTable = () => {
   return (
     <>
       <TitleBar>
-        <IconButton icon='ITEMS.LIST' selected={showFilter} onClick={flipFilter} />
+        <FilterRatio model={model} />
+        <IconButton
+          icon="ITEMS.LIST"
+          selected={showFilter}
+          onClick={flipFilter}
+        />
       </TitleBar>
       <Splitter dir="RIGHT" unfold={showFilter}>
         <Table<string, Property>
diff --git a/ivette/src/renderer/style.css b/ivette/src/renderer/style.css
index 6a2d3ac1a7e..c4fa4266a4e 100644
--- a/ivette/src/renderer/style.css
+++ b/ivette/src/renderer/style.css
@@ -2,9 +2,11 @@
 /* --- Frama-C Styling                                                    --- */
 /* -------------------------------------------------------------------------- */
 
-.controller-rank {
-    color: #888 ;
+.component-info {
+    color: #888;
     min-width: 50px;
+    padding-top: 4px;
+    font-size: smaller;
 }
 
 .code-column {
-- 
GitLab