src/trace_js.ml.str

   1 var old_timer = null;
   2 var old_node = null;
   3
   4 var make_button = function (target, label)
   5 {
   6     var msg  = '<button onclick="';
   7     msg += 'activate(\'' + target + '\')"';
   8     if (target == 'node-1') msg+= ' disabled="disabled" ';
   9     msg+= '>' + label + '</button>';
  10     return msg;
  11 };
  12
  13 var activate = function (id)
  14 {
  15     if (old_node) {
  16         clearInterval(old_timer);
  17         old_node.style.fillOpacity = 1.0;
  18         old_node.style.stroke = 'black';
  19         old_node.classList.remove('blink');
  20     };
  21     var node = document.getElementById(id);
  22     var div = document.getElementById('svg');
  23     var node_dim = node.getBBox();
  24     var div_dim = div.getBoundingClientRect();
  25     var nx = node_dim.x;
  26     var ny = node_dim.y;
  27     var hs = nx - (div_dim.width / 2 - node_dim.width / 2);
  28     var vs = ny - (div_dim.height / 2 - node_dim.height / 2);
  29     div.scrollLeft = hs;
  30     div.scrollTop = vs;
  31     node.style.stroke = 'red';
  32     old_node = node;
  33     node.classList.add('blink');
  34
  35     var d = document.getElementById('data');
  36     var msg = '';
  37     for (i=0; i < rounds; i++)
  38         msg += ('<p>round: ' + i + ':<br/>') + data[i][id] + '</p>\n';
  39
  40     var rect = document.getElementById(id);
  41     var fce = rect.firstElementChild;
  42     var nse = fce.nextElementSibling;
  43     var pare = nse.nextElementSibling;
  44     var pse = pare.nextElementSibling;
  45     var fc = fce.textContent;
  46     var ns = nse.textContent;
  47     var par = pare.textContent;
  48     var ps = pse.textContent;
  49     msg += make_button(par, "↑");
  50     msg += make_button(ps, "←");
  51     msg += make_button(fc, "↓");
  52     msg += make_button(ns,"→");
  53     d.innerHTML = msg;
  54     return;
  55 };