diff --git a/ivette/api/plugins/dive/index.ts b/ivette/api/plugins/dive/index.ts
index 2aa5ba25a756f9ff7fa5362f6dfc5150b2e77b0c..8223fb299d73cb2b8f519ce2789ba1a4c0547fa7 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 18ab59f9bf2e484b5d25cafa2e46e30c356378a1..d2e594777b410a85d98997b68ad38438ea912027 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 5f74f23af898a30d7d6c39923280bc2d6c85a0fc..826b52e8d663f04ff3c7d421edabcabe75923ee6 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