[dive] fix a bug where clicking several time on a node with a unique...

[dive] fix a bug where clicking several time on a node with a unique dependency would not select the dependency

ivette/src/frama-c/dive/Dive.tsx

@@ -486,15 +486,12 @@ class Dive {
     );
     this.cy.$(':selected').forEach(unselect);
     this.cy.$('.multiple-selection').removeClass('multiple-selection');
+    this.cy.$('.selection').removeClass('selection');
     select(node);
     const edges = node.incomers('edge');
-    edges.addClass('multiple-selection');
-    edges.unselect();
     const relevantEdges = edges.filter(hasOrigin);
-    if (relevantEdges.empty())
-      edges.select();
-    else
-      relevantEdges.select();
+    edges.addClass('multiple-selection');
+    relevantEdges.addClass('selection');
   }
 }
 

ivette/src/frama-c/dive/style.json

@@ -15,14 +15,6 @@
       "text-wrap" : "wrap"
     }
   },
-  {
-    "selector": "node:selected",
-    "style": {
-      "overlay-color": "#8bf",
-      "overlay-padding": "10px",
-      "overlay-opacity": 0.4
-    }
-  },
   {
     "selector": "node[label]",
     "style": {
@@ -58,7 +50,7 @@
     }
   },
   {
-    "selector": ".multiple-selection",
+    "selector": "edge.multiple-selection",
     "style": {
       "overlay-color": "#aaa",
       "overlay-padding": "10px",
@@ -66,9 +58,8 @@
     }
   },
   {
-    "selector": "edge:selected",
+    "selector": "edge.selection, :selected",
     "style": {
-      "color": "#48f",
       "overlay-color": "#8bf",
       "overlay-padding": "10px",
       "overlay-opacity": 0.4