Refactor the tracing code, store the whole tree structure in a javascript array and...

[tatoo.git] / src / trace_js.ml.str

diff --git a/src/trace_js.ml.str b/src/trace_js.ml.str
index 4d17382..53af07c 100644 (file)
--- a/src/trace_js.ml.str
+++ b/src/trace_js.ml.str
@@ -1,24 +1,47 @@
 // -*-Javascript-*-
-var old_timer = null;
-var old_node = null;
 
-var make_button = function (target, label)
-{
-    var msg  = '<button onclick="';
-    msg += 'activate(\'' + target + '\')"';
-    if (target == 'node-1') msg+= ' disabled="disabled" ';
-    msg+= '>' + label + '</button>';
-    return msg;
+var hide_nodes = function () {
+    var v = document.getElementById('relnodes').value;
+    for(i = 0; i < last_id; i++) {
+       var id = 'node' + i;
+       var rect = document.getElementById(id);
+
+       if ((v-0) <= tree[id].max)
+           rect.style.fillOpacity = 1;
+       else
+           rect.style.fillOpacity = 0.3;
+    }
 };
 
+var activate_parent = function () {
+    if (current_node) activate(tree[current_node].par);
+};
+var activate_previous = function () {
+    if (current_node) activate(tree[current_node].ps);
+};
+var activate_next = function () {
+    if (current_node) activate(tree[current_node].ns);
+};
+var activate_first = function () {
+    if (current_node) activate(tree[current_node].fc);
+};
+var buttons = document.getElementsByTagName("button");
 var activate = function (id)
 {
-    if (old_node) {
-        clearInterval(old_timer);
-        old_node.style.fillOpacity = 1.0;
-        old_node.style.stroke = 'black';
-        old_node.classList.remove('blink');
+    if (id == nil_id) return;
+    if (current_node) {
+       var rect = document.getElementById(current_node);
+        rect.style.fillOpacity = 1.0;
+        rect.style.stroke = 'black';
+        rect.classList.remove('blink');
     };
+    hide_nodes();
+    current_node = id;
+    buttons[0].disabled = tree[id].par == nil_id;
+    buttons[1].disabled = tree[id].ps == nil_id;
+    buttons[2].disabled = tree[id].fc == nil_id;
+    buttons[3].disabled = tree[id].ns == nil_id;
+
     var node = document.getElementById(id);
     var div = document.getElementById('svg');
     var node_dim = node.getBBox();
@@ -35,22 +58,9 @@ var activate = function (id)
 
     var d = document.getElementById('data');
     var msg = '';
-    for (i=0; i < rounds; i++)
-       msg += ('<p>round: ' + i + ':<br/>') + data[i][id] + '</p>\n';
-
-    var rect = document.getElementById(id);
-    var fce = rect.firstElementChild;
-    var nse = fce.nextElementSibling;
-    var pare = nse.nextElementSibling;
-    var pse = pare.nextElementSibling;
-    var fc = fce.textContent;
-    var ns = nse.textContent;
-    var par = pare.textContent;
-    var ps = pse.textContent;
-    msg += make_button(par, "↑");
-    msg += make_button(ps, "←");
-    msg += make_button(fc, "↓");
-    msg += make_button(ns,"→");
+    for (i=0; i <= rounds; i++)
+       msg += ('<p>round ' + i + ':<br/>new states:') + tree[id].dlist[i]
+    + '<br/>all states:' + tree[id].flist[i] + '</p>\n';
     d.innerHTML = msg;
     return;
 };