src/trace_js.ml.str

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