[FEAT] graphexplorer: SHIFT key equivalent to 'add' checkbox

static/lib/graphExplorer/extras_explorerjs.js

@@ -86,7 +86,14 @@ function CRUD( list_id , ngram_ids , http_method , callback) {
 }
 
 
+// general listener: shift key in the window <=> add to selection
+$(document).on('keyup keydown', function(e){
+  // changes the global boolean ("add node to selection" status) if keydown and SHIFT
+  checkBox = e.shiftKey
 
+  // show it in the real checkbox too
+  $('#checkboxdiv').prop("checked", e.shiftKey)
+} );
 
 // = = = = = = = = = = = [ Clusters Plugin ] = = = = = = = = = = = //
 
@@ -982,6 +989,7 @@ function camaraButton(){
     });
 }
 
+
 function getTips(){
     console.log('FUN extras_explorerjs:getTips')
     param='';

static/lib/graphExplorer/tinawebJS/Tinaweb.js

@@ -510,6 +510,7 @@ TinaWebJS = function ( sigmacanvas ) {
                 }
             }
         });
+
     }
 
     //  external usage: SelectorEngine*() , MultipleSelection2() ,
@@ -522,7 +523,6 @@ TinaWebJS = function ( sigmacanvas ) {
 
         $("#closeloader").click();
 
-
         $('.etabs').click(function(){
             $.doTimeout(500,function () {
                 $("#opossiteNodes").readmore({maxHeight:200});