Graph editor: remove node_id from node_id_to_dom_element_id when node is removed (from Ioannis)

dream/platform/src/jsplumb/jsplumb.js

@@ -313,6 +313,7 @@
     );
     $(gadget.props.element).find("#" + element_id).remove();
     delete gadget.props.data.graph.node[node_id];
+    delete gadget.props.data.node_id_to_dom_element_id[node_id];
 
     $.each(gadget.props.data.graph.edge, function (k, v) {
       if (node_id === v.source || node_id === v.destination) {