X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Ftrace_js.ml.str;fp=src%2Ftrace_js.ml.str;h=53af07c14bfa1f98986cd61905998aa4b730e552;hp=4d17382f217cbe81160d32f4b4e290be1610b999;hb=a089738aa464521c0ae79944eb00fc147cc37ac9;hpb=22f564fb392fd71207e19cc862c0a18c34d1c2c0

diff --git a/src/trace_js.ml.str b/src/trace_js.ml.str
index 4d17382..53af07c 100644
--- 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;
 };