From 36d91c6af372a53a8691eb97545a3217559e8d20 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 24 Jul 2020 15:26:13 +0200
Subject: [PATCH] [ivette] Dive: fix context menu and hide action
---
ivette/api/plugins/dive/index.ts | 9 ++-
ivette/src/frama-c/dive/Dive.tsx | 111 ++++++++++++---------------
src/plugins/dive/server_interface.ml | 2 +-
3 files changed, 53 insertions(+), 69 deletions(-)
diff --git a/ivette/api/plugins/dive/index.ts b/ivette/api/plugins/dive/index.ts
index 2aa5ba25a75..8223fb299d7 100644
--- a/ivette/api/plugins/dive/index.ts
+++ b/ivette/api/plugins/dive/index.ts
@@ -238,12 +238,13 @@ export const byGraphData: Compare.Order<graphData> =
/** Graph differences from the last action. */
export type diffData =
- { root: nodeId, add: { nodes: node[], deps: dependency[] }, sub: nodeId[] };
+ { root?: nodeId, add: { nodes: node[], deps: dependency[] }, sub: nodeId[]
+ };
/** Loose decoder for `diffData` */
export const jDiffData: Json.Loose<diffData> =
Json.jObject({
- root: jNodeIdSafe,
+ root: jNodeId,
add: Json.jFail(
Json.jObject({
nodes: Json.jArray(jNodeSafe),
@@ -259,9 +260,9 @@ export const jDiffDataSafe: Json.Safe<diffData> =
/** Natural order for `diffData` */
export const byDiffData: Compare.Order<diffData> =
Compare.byFields
- <{ root: nodeId, add: { nodes: node[], deps: dependency[] },
+ <{ root?: nodeId, add: { nodes: node[], deps: dependency[] },
sub: nodeId[] }>({
- root: byNodeId,
+ root: Compare.defined(byNodeId),
add: Compare.byFields
<{ nodes: node[], deps: dependency[] }>({
nodes: Compare.array(byNode),
diff --git a/ivette/src/frama-c/dive/Dive.tsx b/ivette/src/frama-c/dive/Dive.tsx
index 18ab59f9bf2..d2e594777b4 100644
--- a/ivette/src/frama-c/dive/Dive.tsx
+++ b/ivette/src/frama-c/dive/Dive.tsx
@@ -26,34 +26,32 @@ import '@fortawesome/fontawesome-free/js/all';
import style from './style.json';
import layouts from './layouts.json';
-const ctxmenu = {
- explore: <div><div className="fas fa-binoculars fa-2x" />Explore</div>,
- unfold: <div><div className="fa fa-expand-arrows-alt fa-2x" />Unfold</div>,
- fold: <div><div className="fa fa-compress-arrows-alt fa-2x" />Fold</div>,
- show: <div><div className="fa fa-eye fa-2x" />Show</div>,
- hide: <div><div className="fa fa-eye-slash fa-2x" />Hide</div>,
-};
-
-export interface Callsite {
- readonly fun: string;
- readonly instr: string;
-}
-
-export interface Interval {
- readonly min: number;
- readonly max: number;
+interface Cxtcommand {
+ content: string;
+ select: () => void;
+ enabled: boolean;
}
-export type callstack = Callsite[];
-
interface CytoscapeExtended extends Cytoscape.Core {
cxtmenu(options: any): void;
}
-function callstackToString(callstack: callstack): string {
+function callstackToString(callstack: API.callstack[]): string {
return callstack.map((cs) => `${cs.fun}:${cs.instr}`).join('/');
}
+function buildCxtMenu(
+ commands: Cxtcommand[],
+ content? : JSX.Element,
+ action? : () => void,
+) {
+ commands.push({
+ content: content ? renderToString(content) : '',
+ select: action || (() => {}),
+ enabled: !!action,
+ });
+}
+
/* The Dive class handles the selection of nodes according to user actions.
To prevent cytoscape to automatically select (and unselect) nodes wrongly,
we make some nodes unselectable. We then use the functions below to make
@@ -85,58 +83,42 @@ class Dive {
this.cy = cy || Cytoscape();
this.headless = this.cy.container() === null;
this.cy.elements().remove();
- this.cy.off('click');
+ this.cy.off('click'); // Remove previous listeners
this.cy.on('click', 'node', (event) => this.clickNode(event.target));
this.layout = 'cose-bilkent';
- if (!this.headless)
- this.setupCtxMenu();
+ if (!this.headless) {
+ this.cy.scratch('cxtmenu')?.destroy?.(); // Remove previous menu
+ this.cy.scratch('cxtmenu', (this.cy as CytoscapeExtended).cxtmenu({
+ selector: 'node',
+ commands: (node: Cytoscape.NodeSingular) => this.onCxtMenu(node),
+ }));
+ }
this.refresh();
}
- setupCtxMenu(): void {
- (this.cy as CytoscapeExtended).cxtmenu({
- selector: 'node',
- commands: (ele: Cytoscape.NodeSingular) => {
- const data = ele.data();
- const commands = [{
- content: renderToString(ctxmenu.explore),
- select: () => { this.explore(ele); },
- enabled: true,
- }];
- if (data.kind === 'composite') {
- commands.push({
- content: renderToString(ctxmenu.unfold),
- select: () => {},
- enabled: false,
- });
- }
- else {
- commands.push({
- content: '',
- select: () => {},
- enabled: false,
- });
- }
- if (!data.explored) {
- commands.push({
- content: renderToString(ctxmenu.show),
- select: () => this.show(ele),
- enabled: true,
- });
- }
- else {
- commands.push({
- content: renderToString(ctxmenu.hide),
- select: () => this.hide(ele),
- enabled: true,
- });
- }
- return commands;
- },
- });
+ onCxtMenu(node: Cytoscape.NodeSingular) {
+ const data = node.data();
+ const commands = [] as Cxtcommand[];
+ buildCxtMenu(commands,
+ <><div className="fas fa-binoculars fa-2x" />Explore</>,
+ () => { this.explore(node); });
+ if (data.kind === 'composite')
+ buildCxtMenu(commands,
+ <><div className="fa fa-expand-arrows-alt fa-2x" />Unfold</>);
+ else
+ buildCxtMenu(commands);
+ if (data.backward_explored === 'no')
+ buildCxtMenu(commands,
+ <div><div className="fa fa-eye fa-2x" />Show</div>,
+ () => this.show(node));
+ else
+ buildCxtMenu(commands,
+ <><div className="fa fa-eye-slash fa-2x" />Hide</>,
+ () => this.hide(node));
+ return commands;
}
remove(node: Cytoscape.NodeCollection): void {
@@ -156,7 +138,8 @@ class Dive {
return this.cy.add({ data: { id, label: fileName }, classes: 'file' });
}
- referenceCallstack(callstack: callstack): Cytoscape.NodeSingular | null {
+ referenceCallstack(callstack: API.callstack[]): Cytoscape.NodeSingular | null
+ {
const name = callstackToString(callstack);
const elt = callstack.shift();
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 5f74f23af89..826b52e8d66 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -222,7 +222,7 @@ struct
let name = "diffData"
let descr = Markdown.plain "Graph differences from the last action."
let jtype = Data.declare ~package ~name ~descr (Jrecord [
- "root", NodeId.jtype;
+ "root", Joption NodeId.jtype;
"add", Jrecord [
"nodes", Jarray Node.jtype;
"deps", Jarray Dependency.jtype
--
GitLab