From e38d6fca509198c36f596f4456e0e01768fcbc66 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 24 Jul 2020 09:17:16 +0200
Subject: [PATCH] [ivette] Dive: prevents cytoscape to automatically select
(and unselect) nodes.
---
ivette/src/frama-c/dive/Dive.tsx | 26 ++++++++++++++++++++++----
1 file changed, 22 insertions(+), 4 deletions(-)
diff --git a/ivette/src/frama-c/dive/Dive.tsx b/ivette/src/frama-c/dive/Dive.tsx
index 014dc8cf5fa..55bad9f7466 100644
--- a/ivette/src/frama-c/dive/Dive.tsx
+++ b/ivette/src/frama-c/dive/Dive.tsx
@@ -54,6 +54,21 @@ function callstackToString(callstack: callstack): string {
return callstack.map((cs) => `${cs.fun}:${cs.instr}`).join('/');
}
+/* 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
+ the nodes selectable before (un)selecting them. */
+
+function select(node: Cytoscape.NodeSingular): void {
+ node.selectify();
+ node.select();
+}
+
+function unselect(node: Cytoscape.NodeSingular): void {
+ node.selectify();
+ node.unselect();
+}
+
export type mode = 'explore' | 'overview';
class Dive {
@@ -425,12 +440,15 @@ class Dive {
const writes = node.data()?.writes;
if (writes)
this.onSelect?.(writes);
-
this.selectNode(node);
+ /* Cytoscape automatically selects the node clicked, and unselects all other
+ nodes and edges. As we want some incoming edges to remain selected, we
+ make the node unselectable, preventing cytoscape to select it. */
+ node.unselectify();
}
selectLocation(location: States.Location) {
- const selectNode = this.cy.$(':selected');
+ const selectNode = this.cy.$('node:selected');
const writes = selectNode?.data()?.writes;
if (location.marker && !_.some(writes, location)) {
this.add(location.marker);
@@ -444,8 +462,8 @@ class Dive {
const hasOrigin = (ele: Cytoscape.NodeSingular) => (
_.some(ele.data().origins, this.selectedLocation)
);
- this.cy.$(':selected').unselect();
- node.select();
+ this.cy.$(':selected').forEach(unselect);
+ select(node);
const edges = node.incomers('edge');
edges.unselect();
edges.filter(hasOrigin).select();
--
GitLab