agda-server-0.1: copy/common_en.js

var waiting = 0;
var waitingtimeout;

function getPre(params, cont) {
//    alert('get: ' + params);
    var http = false;
    if (window.XMLHttpRequest) { // Mozilla, Safari,...
        http = new XMLHttpRequest();
        if (http.overrideMimeType) {
            http.overrideMimeType('text/html');
        }
    } else {
        if (window.ActiveXObject) { // IE
            try {
                http = new ActiveXObject("Msxml2.XMLHTTP");
            } catch (e) {
                try {
                    http = new ActiveXObject("Microsoft.XMLHTTP");
                } catch (e) {}
            }
        }
    }
    if (!http) {
        cont('<span class="error">Client error.</span>');
    } else {

//        alert('get ready: x ' );

        if (waiting == 0) {
            waitingtimeout = setTimeout("drawWarning(1);", 1000);
        };
        waiting = waiting + 1;

        http.onreadystatechange = function () {
            if (http.readyState == 4) {
                waiting = waiting - 1;
                if (waiting == 0) {
                    clearTimeout(waitingtimeout);
                    setTimeout("clearWarning();", 500);
                };
                cont(http.responseText);
            }
        }

        http.open('POST', "exercise/", true);
        http.setRequestHeader("Content-type", "application/x-www-form-urlencoded");
        http.setRequestHeader("Content-length", params.length);
        http.setRequestHeader("Connection", "close");
        http.send(params);
    }
}

//////////////////////////////////////////////////

function drawWarning(n) {
    var r="Waiting."; 
    for (var a=0; a< n % 3; a++) r+='.';
    document.getElementById('info').style.display = "block";
    document.getElementById('info').innerHTML = '<div class="wait">' + r + '</div>';
    waitingtimeout = setTimeout('drawWarning(' + (n+1) + ');', 500);
}

function clearWarning() {
    document.getElementById('info').style.display = "none";
    document.getElementById('info').innerHTML = "";
}


//////////////////////////////////////////////////

function resetForms() {
    var forms = document.getElementsByTagName("form");
    for(var index=0;index<forms.length;index++) {
        if (forms[index].className == 'resetinterpreter') { 
            forms[index].reset(); 
        }
    }
}