diff --git a/ivette/api/dive/index.ts b/ivette/api/dive/index.ts
index 7433dc5f951ef5e6340bd3131588a67456345212..a6bfaf5c218247ccaa94194a6cbf491af91056f5 100644
--- a/ivette/api/dive/index.ts
+++ b/ivette/api/dive/index.ts
@@ -68,7 +68,9 @@ export const addVar: Server.ExecRequest<variableName,Json.json> = {
};
/** Add all alarms of the given function */
-export const addFunctionAlarms: Server.ExecRequest<Json.key<'#fct'>,Json.json
+export const addFunctionAlarms: Server.ExecRequest<
+ Json.key<'#fct'>,
+ Json.json
> = {
kind: Server.RqKind.EXEC,
name: 'dive.addFunctionAlarms',
@@ -77,8 +79,7 @@ export const addFunctionAlarms: Server.ExecRequest<Json.key<'#fct'>,Json.json
};
/** Explore the graph starting from an existing vertex */
-export const explore: Server.ExecRequest<Json.index<'#dive-node'>,Json.json
- > = {
+export const explore: Server.ExecRequest<Json.index<'#dive-node'>,Json.json> = {
kind: Server.RqKind.EXEC,
name: 'dive.explore',
input: Json.jIndex<'#dive-node'>('#dive-node'),
diff --git a/ivette/api/kernel/ast/index.ts b/ivette/api/kernel/ast/index.ts
index 0709335396ebe1dc890f19acc57ad79f523f8337..a7c5a9921cba74cb8cee7a84c0c233235be81774 100644
--- a/ivette/api/kernel/ast/index.ts
+++ b/ivette/api/kernel/ast/index.ts
@@ -132,9 +132,11 @@ export const reloadMarkerInfo: Server.GetRequest<null,null> = {
};
/** Data fetcher for array [`markerInfo`](#markerinfo) */
-export const fetchMarkerInfo: Server.GetRequest<number,
+export const fetchMarkerInfo: Server.GetRequest<
+ number,
{ pending: number, updated: markerInfoData[],
- removed: Json.key<'#markerInfo'>[], reload: boolean }> = {
+ removed: Json.key<'#markerInfo'>[], reload: boolean }
+ > = {
kind: Server.RqKind.GET,
name: 'kernel.ast.fetchMarkerInfo',
input: Json.jNumber,
@@ -147,12 +149,13 @@ export const fetchMarkerInfo: Server.GetRequest<number,
};
/** Marker informations */
-export const markerInfo: State.Array<'#markerInfo',markerInfoData> = {
+export const markerInfo: State.Array<Json.key<'#markerInfo'>,markerInfoData> = {
name: 'kernel.ast.markerInfo',
- key: 'key',
+ getkey: ((d:markerInfoData) => d.key),
signal: signalMarkerInfo,
fetch: fetchMarkerInfo,
reload: reloadMarkerInfo,
+ order: byMarkerInfoData,
};
/** Localizable AST markers */
@@ -244,9 +247,11 @@ export const reloadFunctions: Server.GetRequest<null,null> = {
};
/** Data fetcher for array [`functions`](#functions) */
-export const fetchFunctions: Server.GetRequest<number,
+export const fetchFunctions: Server.GetRequest<
+ number,
{ pending: number, updated: functionsData[],
- removed: Json.key<'#functions'>[], reload: boolean }> = {
+ removed: Json.key<'#functions'>[], reload: boolean }
+ > = {
kind: Server.RqKind.GET,
name: 'kernel.ast.fetchFunctions',
input: Json.jNumber,
@@ -259,12 +264,13 @@ export const fetchFunctions: Server.GetRequest<number,
};
/** AST Functions */
-export const functions: State.Array<'#functions',functionsData> = {
+export const functions: State.Array<Json.key<'#functions'>,functionsData> = {
name: 'kernel.ast.functions',
- key: 'key',
+ getkey: ((d:functionsData) => d.key),
signal: signalFunctions,
fetch: fetchFunctions,
reload: reloadFunctions,
+ order: byFunctionsData,
};
/** Get textual information about a marker */
diff --git a/ivette/api/kernel/properties/index.ts b/ivette/api/kernel/properties/index.ts
index f04292d0a807ce6c1a5db679374e4dfb166f4597..3e336583d5a53057486298606d31e163553eb373 100644
--- a/ivette/api/kernel/properties/index.ts
+++ b/ivette/api/kernel/properties/index.ts
@@ -299,9 +299,11 @@ export const reloadStatus: Server.GetRequest<null,null> = {
};
/** Data fetcher for array [`status`](#status) */
-export const fetchStatus: Server.GetRequest<number,
+export const fetchStatus: Server.GetRequest<
+ number,
{ pending: number, updated: statusData[], removed: Json.key<'#status'>[],
- reload: boolean }> = {
+ reload: boolean }
+ > = {
kind: Server.RqKind.GET,
name: 'kernel.properties.fetchStatus',
input: Json.jNumber,
@@ -314,12 +316,13 @@ export const fetchStatus: Server.GetRequest<number,
};
/** Status of Registered Properties */
-export const status: State.Array<'#status',statusData> = {
+export const status: State.Array<Json.key<'#status'>,statusData> = {
name: 'kernel.properties.status',
- key: 'key',
+ getkey: ((d:statusData) => d.key),
signal: signalStatus,
fetch: fetchStatus,
reload: reloadStatus,
+ order: byStatusData,
};
/* ------------------------------------- */
diff --git a/ivette/api/kernel/services/index.ts b/ivette/api/kernel/services/index.ts
index fcfcf35b1fbe3b9ca7c272b7cabd9754cc24bbfa..7da04e4a0aecdd06ad0f69ea83f5219ff28b4a46 100644
--- a/ivette/api/kernel/services/index.ts
+++ b/ivette/api/kernel/services/index.ts
@@ -25,7 +25,8 @@ import { jTagSafe } from 'api/kernel/data';
import { tag } from 'api/kernel/data';
/** Frama-C Kernel configuration */
-export const getConfig: Server.GetRequest<null,
+export const getConfig: Server.GetRequest<
+ null,
{ pluginpath: string[], libdir: string, datadir: string, version: string }
> = {
kind: Server.RqKind.GET,
diff --git a/ivette/api/server_tsc.ml b/ivette/api/server_tsc.ml
index cf88117b4e226d996c27038e15d42c83d758f537..3df4c37188eb1893a0b0020b50800d5654a96324 100644
--- a/ivette/api/server_tsc.ml
+++ b/ivette/api/server_tsc.ml
@@ -311,7 +311,7 @@ let makeDeclaration fmt names d =
let output = typeOfParam rq.rq_output in
let makeParam fmt js = makeDecoder ~safe:false ~names fmt js in
Format.fprintf fmt
- "@[<hov 2>export const %s: Server.%sRequest<@,%a,@,%a@,> = {@]@\n"
+ "@[<hv 2>export const %s: Server.%sRequest<@,%a,@,%a@,>@] = {@\n"
self.name prefix jtype input jtype output ;
Format.fprintf fmt " kind: Server.RqKind.%s,@\n" kind ;
Format.fprintf fmt " name: '%s',@\n" (Pkg.name_of_ident d.d_ident) ;
@@ -321,7 +321,7 @@ let makeDeclaration fmt names d =
| D_value js ->
Format.fprintf fmt
- "@[<hov 2>export const %s: State.Value<@,%a@,> = {@]@\n"
+ "@[<hv 2>export const %s: State.Value<@,%a@,>@] = {\n"
self.name jtype js ;
Format.fprintf fmt " name: '%s',@\n" (Pkg.name_of_ident self) ;
Format.fprintf fmt " signal: %a,@\n"
@@ -332,7 +332,7 @@ let makeDeclaration fmt names d =
| D_state js ->
Format.fprintf fmt
- "@[<hov 2>export const %s: State.State<@,%a@,> = {@]@\n"
+ "@[<hv 2>export const %s: State.State<@,%a@,>@] = {@\n"
self.name jtype js ;
Format.fprintf fmt " name: '%s',@\n" (Pkg.name_of_ident self) ;
Format.fprintf fmt " signal: %a,@\n"
@@ -345,34 +345,38 @@ let makeDeclaration fmt names d =
| D_array { arr_key ; arr_kind } ->
let data = Pkg.Derived.data self in
+ let jkey = (Pkg.Jkey arr_kind) in
+ let jrow = (Pkg.Jdata data) in
Format.fprintf fmt
- "@[<hov 2>export const %s: State.Array<@,'#%s',@,%a@,> = {@]@\n"
- self.name arr_kind (jcall names) data ;
+ "@[<hv 2>export const %s: State.Array<@,%a,@,%a@,>@] = {@\n"
+ self.name jtype jkey jtype jrow ;
Format.fprintf fmt " name: '%s',@\n" (Pkg.name_of_ident self) ;
- Format.fprintf fmt " key: '%s',@\n" arr_key ;
+ Format.fprintf fmt " getkey: ((d:%a) => d.%s),@\n" jtype jrow arr_key ;
Format.fprintf fmt " signal: %a,@\n"
(jcall names) (Pkg.Derived.signal self) ;
Format.fprintf fmt " fetch: %a,@\n"
(jcall names) (Pkg.Derived.fetch self) ;
Format.fprintf fmt " reload: %a,@\n"
(jcall names) (Pkg.Derived.reload self) ;
+ Format.fprintf fmt " order: %a,@\n"
+ (jcall names) (Pkg.Derived.order data) ;
Format.fprintf fmt "};@\n"
| D_safe(id,js) ->
Format.fprintf fmt
- "@[<hov 2>export const %s: Json.Safe<@,%a@,> =@ %a;@]\n"
+ "@[<hov 2>@[<hv 0>export const %s: Json.Safe<@,%a@,>@] =@ %a;@]\n"
self.name (jcall names) id
(makeRecursive (makeRootDecoder ~safe:true ~self:id ~names)) js
| D_loose(id,js) ->
Format.fprintf fmt
- "@[<hov 2>export const %s: Json.Loose<@,%a@,> =@ %a;@]\n"
+ "@[<hov 2>@[<hv 0>export const %s: Json.Loose<@,%a@,>@] =@ %a;@]\n"
self.name (jcall names) id
(makeRecursive (makeRootDecoder ~safe:false ~self:id ~names)) js
| D_order(id,js) ->
Format.fprintf fmt
- "@[<hov 2>export const %s: Compare.Order<@,%a@,> =@ %a;@]\n"
+ "@[<hov 2>@[<hv 0>export const %s: Compare.Order<@,%a@,>@] =@ %a;@]\n"
self.name (jcall names) id
(makeRecursive2 (makeOrder ~self:id ~names)) js
diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx
index 5ec7d4272ee271fe08ada8ae7259e25ae2c9f4cc..5fc898ca878a01c1ea2072d36935ec7d4b4dc806 100644
--- a/ivette/src/renderer/ASTview.tsx
+++ b/ivette/src/renderer/ASTview.tsx
@@ -78,7 +78,7 @@ const ASTview = () => {
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(markerInfo);
+ const markers = States.useSyncModel(markerInfo);
const theFunction = selection?.current?.function;
const theMarker = selection?.current?.marker;
diff --git a/ivette/src/renderer/Globals.tsx b/ivette/src/renderer/Globals.tsx
index 94a501716c0d18f29a6ed499b6cbf46e716ddb99..5d4e1cd82dfa070460a9c419f6aec0fe58d6ca61 100644
--- a/ivette/src/renderer/Globals.tsx
+++ b/ivette/src/renderer/Globals.tsx
@@ -3,10 +3,8 @@
// --------------------------------------------------------------------------
import React from 'react';
-import * as Dome from 'dome';
import { Section, Item } from 'dome/frame/sidebars';
import * as States from 'frama-c/states';
-import { alpha } from 'dome/data/compare';
import { functions, functionsData } from 'api/kernel/ast';
// --------------------------------------------------------------------------
@@ -17,23 +15,9 @@ export default () => {
// Hooks
const [selection, updateSelection] = States.useSelection();
- const model = States.useSyncArray(functions);
- const forceUpdate = Dome.useForceUpdate() as (() => void);
- React.useEffect(() => {
- model.setNaturalOrder((f1, f2) => alpha(f1.name, f2.name));
- const client = model.link();
- client.onReload(forceUpdate);
- client.onUpdate(forceUpdate);
- return client.unlink;
- }, [model, forceUpdate]);
-
- // Functions
- const n = model.getRowCount();
- const fcts: functionsData[] = [];
- for (let i = 0; i < n; i++) {
- fcts.push(model.getRowAt(i));
- }
+ const fcts = States.useSyncArray(functions);
+ // Items
const current: undefined | string = selection?.current?.function;
const makeFctItem = (fct: functionsData) => {
const kf = fct.name;
diff --git a/ivette/src/renderer/Properties.tsx b/ivette/src/renderer/Properties.tsx
index 6e44c4a4d550204ecd981c136c6af1170f36804e..b3b63b9c570e614d5d0cff6cb2f3e3a18f150c2e 100644
--- a/ivette/src/renderer/Properties.tsx
+++ b/ivette/src/renderer/Properties.tsx
@@ -3,12 +3,14 @@
// --------------------------------------------------------------------------
import _ from 'lodash';
-import React from 'react';
+import React, { useEffect } from 'react';
import * as Dome from 'dome';
+import { key } from 'dome/data/json';
import * as States from 'frama-c/states';
import * as Compare from 'dome/data/compare';
import { Label, Code } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
+import * as Models from 'dome/table/models';
import * as Arrays from 'dome/table/arrays';
import { Table, Column, ColumnProps, Renderer } from 'dome/table/views';
import { TitleBar, Component } from 'frama-c/LabViews';
@@ -238,13 +240,13 @@ const byColumn: Arrays.ByColumns<Property> = {
file: Compare.byFields<Property>({ source: byFile }),
};
-class PropertyModel extends Arrays.ArrayModel<Property> {
+class PropertyModel extends Arrays.CompactModel<key<'#status'>, Property> {
private filterFun?: string;
private filterProp = _.cloneDeep(defaultFilter);
constructor() {
- super('key');
+ super((p: Property) => p.key);
this.setOrderingByFields(byProperty);
this.setColumnOrder(byColumn);
this.setFilter(this.filterItem.bind(this));
@@ -410,19 +412,13 @@ 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();
+ Models.useModel(model);
+ const [filtered, total] = [model.getRowCount(), model.getTotalRowCount()];
return (
<Label
className="component-info"
title="Displayed Properties / Total"
- display={filtered !== total}
+ display={filtered !== total || true}
>
{filtered} / {total}
</Label>
@@ -436,8 +432,12 @@ function FilterRatio({ model }: { model: PropertyModel }) {
const RenderTable = () => {
// Hooks
const model = React.useMemo(() => new PropertyModel(), []);
-
- States.useSyncArray<'#status', Property>(Properties.status, model);
+ const data = States.useSyncArray(Properties.status);
+ useEffect(() => {
+ model.removeAllData();
+ model.updateData(data);
+ model.reload();
+ }, [model, data]);
const [selection, updateSelection] = States.useSelection();
@@ -454,8 +454,8 @@ const RenderTable = () => {
// Callbacks
const onPropertySelection = React.useCallback(
- ({ key, function: fct }: Property) => {
- const location = { function: fct, marker: key };
+ ({ key: propKey, function: fct }: Property) => {
+ const location = { function: fct, marker: propKey };
updateSelection({ location });
}, [updateSelection],
);