src/trace_js.ml.str

   1 // -*-Javascript-*-
   2
   3 var hide_nodes = function () {
   4     var v = document.getElementById('relnodes').value;
   5     for(i = 0; i < last_id; i++) {
   6         var id = 'node' + i;
   7         var rect = document.getElementById(id);
   8
   9         if ((v-0) <= tree[id].max)
  10             rect.style.fillOpacity = 1;
  11         else
  12             rect.style.fillOpacity = 0.3;
  13     }
  14 };
  15
  16 var activate_parent = function () {
  17     if (current_node) activate(tree[current_node].par);
  18 };
  19 var activate_previous = function () {
  20     if (current_node) activate(tree[current_node].ps);
  21 };
  22 var activate_next = function () {
  23     if (current_node) activate(tree[current_node].ns);
  24 };
  25 var activate_first = function () {
  26     if (current_node) activate(tree[current_node].fc);
  27 };
  28 var buttons = document.getElementsByTagName("button");
  29 var activate = function (id)
  30 {
  31     if (id == nil_id) return;
  32     if (current_node) {
  33         var rect = document.getElementById(current_node);
  34         rect.style.fillOpacity = 1.0;
  35         rect.style.stroke = 'black';
  36         rect.classList.remove('blink');
  37     };
  38     hide_nodes();
  39     current_node = id;
  40     buttons[0].disabled = tree[id].par == nil_id;
  41     buttons[1].disabled = tree[id].ps == nil_id;
  42     buttons[2].disabled = tree[id].fc == nil_id;
  43     buttons[3].disabled = tree[id].ns == nil_id;
  44
  45     var node = document.getElementById(id);
  46     var div = document.getElementById('svg');
  47     var node_dim = node.getBBox();
  48     var div_dim = div.getBoundingClientRect();
  49     var nx = node_dim.x;
  50     var ny = node_dim.y;
  51     var hs = nx - (div_dim.width / 2 - node_dim.width / 2);
  52     var vs = ny - (div_dim.height / 2 - node_dim.height / 2);
  53     div.scrollLeft = hs;
  54     div.scrollTop = vs;
  55     node.style.stroke = 'red';
  56     old_node = node;
  57     node.classList.add('blink');
  58
  59     var d = document.getElementById('data');
  60     var msg = '';
  61     for (i=0; i <= rounds; i++)
  62         msg += ('<p>round ' + i + ':<br/>new states:') + tree[id].dlist[i]
  63     + '<br/>all states:' + tree[id].flist[i] + '</p>\n';
  64     d.innerHTML = msg;
  65     return;
  66 };