var logdiv : HTMLElement;
var status_node : HTMLElement;
+type PlayerInfo = {
+ dasharray : string,
+}
+var players : { [player: string]: PlayerInfo };
function xhr_post_then(url : string, data: string,
good : (xhr: XMLHttpRequest) => void) {
status_node = document.getElementById('status')!;
status_node.innerHTML = 'js-done';
logdiv = document.getElementById("log")!;
- let dataload = body.dataset.load;
+ let dataload = JSON.parse(body.dataset.load!);
+ players = dataload.players!;
delete body.dataset.load;
space = svg_element('space')!;