-function resume()
-{
- advanceButton.disabled = false;
- retractButton.disabled = false;
- cursorButton.disabled = false;
- bottomButton.disabled = false;
-}
-
-function advanceForm1(cb)
-{
- var req = null;
- pause();
- if (window.XMLHttpRequest)
- {
- req = new XMLHttpRequest();
- }
- else if (window.ActiveXObject)
- {
- try {
- req = new ActiveXObject("Msxml2.XMLHTTP");
- } catch (e)
- {
- try {
- req = new ActiveXObject("Microsoft.XMLHTTP");
- } catch (e) {}
- }
- }
- req.onreadystatechange = function()
- {
-
- rs = req.readyState;
- stat = req.status;
- stxt = req.statusText;
-
- if(rs == 4)
- {
- var len;
- if(stat == 200)
- {
- debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
- response = req.responseText.split("@");
- len = parseInt(response[0]);
- len0 = unlocked.innerHTML.length;
- unescaped = unlocked.innerHTML.unescapeHTML();
- parsedtxt = unescaped.substr(0,len);
- unparsedtxt = unescaped.substr(len);
- locked.innerHTML = locked.innerHTML + parsedtxt;
- unlocked.innerHTML = unparsedtxt;
- len1 = unlocked.innerHTML.length;
- len2 = len0 - len1;
- populate_goalarray(response[1]);
- statements = listcons(len2,statements);
- unlocked.scrollIntoView(true);
- }
- else
- {
- debug("advance error: returned status code " + req.status + " " + req.statusText + "\n" +
- req.responseText);
- len = 0;
- }
- resume();
- if (cb) {
- cb(len);
- }
- }
- };
- req.open("POST", "advance"); // + escape(unlocked.innerHTML), true);
- req.send(unlocked.innerHTML.unescapeHTML());
-
-}
-
-function gotoBottom()
-{
- var req = null;
- pause();
- if (window.XMLHttpRequest)
- {
- req = new XMLHttpRequest();
- }
- else if (window.ActiveXObject)
- {
- try {
- req = new ActiveXObject("Msxml2.XMLHTTP");
- } catch (e)
- {
- try {
- req = new ActiveXObject("Microsoft.XMLHTTP");
- } catch (e) {}
- }
- }
- req.onreadystatechange = function()
- {
-
- rs = req.readyState;
- stat = req.status;
- stxt = req.statusText;
-
- if(rs == 4)
- {
- if(stat == 200)
- {
- debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
- response = req.responseText.split("@");
- len = parseInt(response[0]);
- len0 = unlocked.innerHTML.length;
- unescaped = unlocked.innerHTML.unescapeHTML();
- parsedtxt = unescaped.substr(0,len);
- unparsedtxt = unescaped.substr(len);
- locked.innerHTML = locked.innerHTML + parsedtxt;
- unlocked.innerHTML = unparsedtxt;
- len1 = unlocked.innerHTML.length;
- len = len0 - len1;
- populate_goalarray(response[1]);
- statements = listcons(len,statements);
- unlocked.scrollIntoView(true);
- }
- else
- {
- debug("goto bottom error: returned status code " + req.status + " " + req.statusText + "\n" +
- req.responseText);
- }
- resume();
- }
- };
- req.open("POST", "bottom"); // + escape(unlocked.innerHTML), true);
- req.send(unlocked.innerHTML.unescapeHTML());
-
-}
-
-function gotoPos(offset)
-{
- if (!offset) {
- offset = getCursorPos();
- }
- if (offset > 0) {
- advanceForm1(function(len) {
- gotoPos(offset-len)
- });
- }
-
-}
-
-function retract()
-{
- var req = null;
- if (window.XMLHttpRequest)
- {
- req = new XMLHttpRequest();
- }
- else if (window.ActiveXObject)
- {
- try {
- req = new ActiveXObject("Msxml2.XMLHTTP");
- } catch (e)
- {
- try {
- req = new ActiveXObject("Microsoft.XMLHTTP");
- } catch (e) {}
- }
- }
- req.onreadystatechange = function()
- {
-
- rs = req.readyState;
- stat = req.status;
- stxt = req.statusText;
-
- if(rs == 4)
- {
- if(stat == 200)
- {
- debug("retract: received response\nBEGIN\n" + req.responseText + "\nEND");
- response = req.responseText;
- statementlen = parseInt(listhd(statements));
- statements = listtl(statements);
- lockedlen = locked.innerHTML.length - statementlen;
- statement = locked.innerHTML.substr(lockedlen, statementlen);
- locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
- unlocked.innerHTML = statement + unlocked.innerHTML;
- populate_goalarray(response);
- unlocked.scrollIntoView(true);
- }
- else
- {
- debug("retract error: returned status code " + req.status + " " + req.statusText + "\n" +
- req.responseText);
- }
- resume();
- }
- };
- req.open("GET", "retract"); // + escape(unlocked.innerHTML), true);
- req.send();
-
-}
-
-function openFile()
-{
- var req = null;
- if (window.XMLHttpRequest)
- {
- req = new XMLHttpRequest();
- }
- else if (window.ActiveXObject)
- {
- try {
- req = new ActiveXObject("Msxml2.XMLHTTP");
- } catch (e)
- {
- try {
- req = new ActiveXObject("Microsoft.XMLHTTP");
- } catch (e) {}
- }
- }
- req.onreadystatechange = function()
- {
-
- rs = req.readyState;
- stat = req.status;
- stxt = req.statusText;
-
- if(rs == 4)
- {
- if(stat == 200)
- {
- locked.innerHTML = "";
- unlocked.innerHTML = req.responseText;
- }
- else
- {
- debug("open error: returned status code " + req.status + " " + req.statusText + "\n" +
- req.responseText);
- }
- }
- };
- req.open("GET", "open?file=" + escape(filename.value), true);
- req.send();
-}
-
-var goalcell;
-
-function hideSequent() {
- goalcell.parentNode.removeChild(goalcell);
- scriptcell.setAttribute("colspan","2");
-}
-
-function showSequent() {
- scriptcell.setAttribute("colspan","1");
- workarea.appendChild(goalcell);
-}
-
-function removeElement(id) {
- var element = document.getElementById(id);
- element.parentNode.removeChild(element);
-}
-
-function getCursorPos() {
- var cursorPos;
- if (window.getSelection) {
- var selObj = window.getSelection();
- var selRange = selObj.getRangeAt(0);
- //cursorPos = findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
- cursorPos = findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
- /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
- return(cursorPos);
- }
- else if (document.selection) {
- var range = document.selection.createRange();
- var bookmark = range.getBookmark();
- /* FIXME the following works wrong when the document is longer than 65535 chars */
- cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
- return(cursorPos);
- }
-}