diff options
Diffstat (limited to 'docs/chapter22/index.html')
| -rw-r--r-- | docs/chapter22/index.html | 218 |
1 files changed, 218 insertions, 0 deletions
diff --git a/docs/chapter22/index.html b/docs/chapter22/index.html new file mode 100644 index 00000000..06e19e2c --- /dev/null +++ b/docs/chapter22/index.html @@ -0,0 +1,218 @@ +<!DOCTYPE html style="height: 100%; margin:0"> +<meta charset="utf-8"> +<title>Simple Viewer</title> +<script src="d3.v7.min.js"></script> +<script src="graphviz.umd.js"></script> +<script src="d3-graphviz.js"></script> + +<body style="height: 100%; margin:0"> + + <div style="display:flex; flex-flow:column; height: 100%;"> + <div style="position:fixed; top:0; left:0; height:20%; width:30%;" > + <div align="center" >Simple Program:</div> + <textarea + id="program" + autofocus="true" + name="Program" + defaultValue="return 0;" + ></textarea> + </div> + <div id="fill" style="flex: 1 1 auto"> </div> + <div id="graph" style="flex: 0 1 auto; align-self:center;"> </div> + + <div style="display:flex; flex-flow:row; flex: 0 1 auto; align-self:center;"> + <style> + .button { color:white; background-color:black; font-size:20px; min-width:30px } + </style> + <button id="doPrev" type="button" onclick="doPrev()" class="button">⮜</button> + <div id="N" style="font-size: 20px; border-style: ridge; min-width: 50px; text-align: right; padding-right: 10px;">0</div> + <button id="doNext" type="button" onclick="doNext()" class="button">⮞</button> + <div id="len" style="font-size: 20px; min-width: 50px; text-align: right; padding-right: 10px;">0</div> + <button id="doExit" type="button" onclick="doExit()" class="button">Exit</button> + </div> + </div> + + +<script> + + var _timer; // Shutdown timer if server goes silent + var N=0 ; // Which dot/graph is being displayed + var dots=[]; // An array of DOT strings + var done; // No more DOTs from server + // Graphviz renderer + var graphviz = d3.select("#graph").graphviz() + .transition(function () { + return d3.transition("main") + .ease(d3.easeLinear) + .delay(0) + .duration(500); + }); + + // Websocket. :-P + const socket = new WebSocket("ws://localhost:12345"); + + // Read user program + const DOC_PROG = document.getElementById('program'); + // Default value seems to be ignored??? + DOC_PROG.value="return 0;"; + function get_program() { + console.log("get_program"); + var src = DOC_PROG.value; + console.log(src); + // Reset visualizer state before sending + updateN(0); + dots=[]; + done=false; + // Send program; will start getting DOT frames shortly + socket.send(src); + // Once the program is sent, timer starts + _timer = setTimeout("close()",100000) + }; + DOC_PROG.onchange=get_program; + + // Go forwards in the animation + function doNext() { + updateN(N+1); + if( N < dots.length ) { + render(N-1,N,1); + } else { + N = dots.length; + socket.send("+"); // Block awaiting server next frame + } + } + + // Go back in the animation + function doPrev() { + if( N>0 ) { + updateN(N-1); + if( N < dots.length-1 ) { + render(N+1,N,-1); + } + } + } + + // exit + function doExit() { socket.send(null); close(); }; + + // Update step counter display and buttons + function updateN(newN) { + N = newN; + DOC_PREV = document.getElementById("doPrev"); + DOC_NEXT = document.getElementById("doNext"); + + if( N==0 && !DOC_PREV.disabled ) { + DOC_PREV.disabled = true; + DOC_PREV.style.backgroundColor = "grey"; + } + if( N>0 && DOC_PREV.disabled ) { + DOC_PREV.disabled = false; + DOC_PREV.style.backgroundColor = "black"; + } + if( N <dots.length && DOC_NEXT.disabled ) { + // Indicate stall, no next frame from server + DOC_NEXT.textContent = "\u2B9E"; + DOC_NEXT.disabled = false; + DOC_NEXT.style.backgroundColor = "black"; + } + if( N==dots.length && !DOC_NEXT.disabled ) { + // Indicate stall, no next frame from server + DOC_NEXT.textContent = "..."; + DOC_NEXT.disabled = true; + DOC_NEXT.style.backgroundColor = "grey"; + } + document.getElementById("N") .textContent = N==dots.length ? (">"+(N-1)) : N; + document.getElementById("len").textContent = dots.length; + }; + + + // Render an animation, from idx to end by step. + // 'end' is inclusive. + var renderActive = -1; + function render(idx, end, step) { + old = renderActive; + renderActive = (end+step); + // No active, so start rendering + if( old == -1 ) + _rend(idx,end+step,step); + } + // Render an animation in a 'for' loop of frames + // until we hit the end. Looping is done via callbacks. + // end is exclusive. + var aix = -1; // Last DOT rendered + function _rend(idx,end,step) { + // Skip animation if already rendered/showing on screen + if( idx==aix ) _rendNext(idx,end,step); + else { + aix = idx; + var str = dots[idx].indexOf("// POS: "); + console.log(str); + if( str == -1 ) DOC_PROG.setSelectionRange(0,0); + else { + var pos = Number(dots[idx].substring(str+8,str+12)); + console.log(pos,pos+1); + document.getElementById("program").focus(); + document.getElementById("program").setSelectionRange(pos,pos+1); + } + graphviz.renderDot(dots[idx]).on("end", () => _rendNext(idx,end,step)) + } + } + function _rendNext(idx,end,step) { + // Not at end so... + if( idx+step != end ) + // Render next step + _rend(idx+step,end,step); + else { + // All desired frames rendered + if( renderActive == end ) { + renderActive = -1; // all frames done + } else { + // Skip-a-few and render the last asked for + _rend(renderActive-1,renderActive,1) + } + } + }; + + + socket.onopen = () => { console.log('WebSocket connection opened'); }; + + // receive message from server; either a shutdown or a new graph + socket.onmessage = (event) => { + clearTimeout(_timer); _timer=null; + const dot = event.data; + console.log("Received:", dot.substring(0,40)); + + if( dot == "!" ) { + // Server requests client resets + get_program(); + + } else if( dot == "#" ) { + // Server sent final frame + done = true; + + } else if( dot.startsWith("digraph") ) { + // Received a new graph + dots.push(dot); + //console.log(dot); + updateN(N); + socket.send("+"); // Get another frame + // If at-end, receiving a graph immediately renders + if( dots.length==1 ) + graphviz.renderDot(dots[0]); + else if( N+1 == dots.length ) + render(N-1,N,1); + // After render, hang around until user clicks things + console.log("GRAPHVIZ done; N="+N+"; dots="+dots.length); + + } else { + console.error('Server sent unexpected: ',dot); + get_program(); + } + }; + + socket.onclose = () => { close(); } + socket.onerror = (error) => { + console.error('WebSocket error:', error); + }; + +</script> +</body> |