From: Wilmer Ricciotti Date: Wed, 1 Jun 2011 12:29:29 +0000 (+0000) Subject: Matita Web: moved the javascript in a separate file. Bugfixes. X-Git-Tag: make_still_working~2472 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1d74bd1321f8b95291efb354428d9ddc36cf8716;p=helm.git Matita Web: moved the javascript in a separate file. Bugfixes. --- diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html index fa119b5ba..8a3641863 100644 --- a/matitaB/matita/index.html +++ b/matitaB/matita/index.html @@ -3,525 +3,7 @@ - + diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index f6e686c53..6601400ed 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -142,8 +142,8 @@ let retract () = match !history with _::(status::_ as history) -> history, status - | [_] -> failwith "retract" - | _ -> assert false in + | [_] -> (prerr_endline "singleton";failwith "retract") + | _ -> (prerr_endline "nil"; assert false) in NCicLibrary.time_travel !status; history := new_history; status := new_status; @@ -275,6 +275,7 @@ let callback req outchan = | "/retract" -> (try let body = retract () in + prerr_endline "retract OK"; Http_daemon.respond ~code:(`Code 200) ~body outchan with e -> (prerr_endline (Printexc.to_string e); diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js new file mode 100644 index 000000000..588643861 --- /dev/null +++ b/matitaB/matita/matitaweb.js @@ -0,0 +1,477 @@ +var locked; +var unlocked; +var workarea; +var scriptcell; +var goalcell; +var goals; +var goalview; +var filename; +var logarea; +var advanceButton; +var retractButton; +var cursorButton; +var bottomButton; +var metasenv = ""; + +function initialize() +{ + locked = document.getElementById("locked"); + unlocked = document.getElementById("unlocked"); + workarea = document.getElementById("workarea"); + scriptcell = document.getElementById("scriptcell"); + goalcell = document.getElementById("goalcell"); + goals = document.getElementById("goals"); + goalview = document.getElementById("goalview"); + filename = document.getElementById("filename"); + logarea = document.getElementById("logarea"); + advanceButton = document.getElementById("advance"); + retractButton = document.getElementById("retract"); + cursorButton = document.getElementById("cursor"); + bottomButton = document.getElementById("bottom"); + + // hide sequent view at start + hideSequent(); +} + +function debug(txt) +{ + logarea.innerHTML = txt + "\n" + logarea.innerHTML; +} + +function listhd(l) +{ + ar = l.split("#"); + debug("hd of '" + l + "' = '" + ar[0] + "'"); + return (ar[0]); +} + +function listtl(l) +{ + i = l.indexOf("#"); + tl = l.substr(i+1); + debug("tl of '" + l + "' = '" + tl + "'"); + return (tl); +} + +function listcons(x,l) +{ + debug("cons '" + x + "' on '" + l + "'"); + return (x + "#" + l); +} + +function listnil() +{ + return (""); +} + +function is_nil(l) +{ + return (l == ""); +} + +function fold_left (f,acc,l) +{ + if (is_nil(l)) + { debug("'" + l + "' is fold end"); + return (acc); } + else + { debug("'" + l + "' is fold cons"); + return(fold_left (f,f(acc,(listhd(l))),listtl(l))); } +} + +function listiter (f,l) +{ + if (is_nil(l)) + { debug("'" + l + "' is nil"); + return; + } + else + { + debug("'" + l + "' is not nil"); + f(listhd(l)); + listiter(f,listtl(l)); + } +} + +function listmap (f,l) +{ + debug("listmap on " + l); + if (is_nil(l)) + { debug("returning listnil"); + return(listnil()); + } + else + { debug("cons f(hd) map(f,tl)"); + return(f(listhd(l)) + "#" + listmap(f,listtl(l))); + } +} + +var statements = listnil(); + +var goalarray; +var metalist = listnil(); + +function pairmap (f,p) +{ + debug("pairmap of '" + p + "'"); + ar = p.split("|"); + return (f(ar[0],ar[1])); +} + +function tripletmap (f,p) +{ + debug("tripletmap of '" + p + "'"); + ar = p.split("|"); + return (f(ar[0],ar[1],ar[2])); +} + +function fst (p) +{ + debug("fst"); + return (pairmap (function (a,b) { return (a); }, p)); +} + +function p13 (p) +{ + debug("p13"); + return (tripletmap (function (a,b,c) { return (a); }, p)); +} + +function p23 (p) +{ + debug("p23"); + return (tripletmap (function (a,b,c) { return (b); }, p)); +} + +function p33 (p) +{ + debug("f33"); + return (tripletmap (function (a,b,c) { return (c); }, p)); +} + +function populate_goalarray(txt) +{ + if (txt == "") { + try { + hideSequent(); + } catch (err) { }; + } else { + showSequent(); + debug("populate with '" + txt + "'"); + goalarray = new Array(); + metalist = listnil(); + var tmp_goallist = ""; + listiter (function(item) + { + debug ("item is '" + item + "'"); + tripletmap (function(a,ahtml,b) { + debug ("found meta n. " + a); + debug ("found goal\nBEGIN" + unescape(b) + "\nEND"); + goalarray[a] = unescape(b); + tmp_goallist = " " + unescape(ahtml) + "" + tmp_goallist; + metalist = listcons(a,metalist); + debug ("goalarray[\"" + a + "\"] = " + goalarray[a]); + },item); + }, txt); + // metalist = listmap (p13,txt); + goals.innerHTML = tmp_goallist; + debug("new metalist is '" + metalist + "'"); + if (is_nil(metalist)) { + switch_goal(); + } + else { + switch_goal(listhd(metalist)); + } + } +} + +function switch_goal(meta) +{ + if (typeof meta == "undefined") { + goalview.innerHTML = ""; + } + else { + debug("switch_goal " + meta + "\n" + goalarray[meta]); + goalview.innerHTML = "Goal ?" + meta + ":\n\n" + goalarray[meta]; + } +} + +String.prototype.unescapeHTML = function() +{ + var patt1 = //gi; + var patt2 = /</gi; + var patt3 = />/gi; + var result = this; + result = result.replace(patt1,"\n"); + result = result.replace(patt2,"<"); + result = result.replace(patt3,">"); + return (unescape(result)); +} + +function pause() +{ + advanceButton.disabled = true; + retractButton.disabled = true; + cursorButton.disabled = true; + bottomButton.disabled = true; +} + +function resume() +{ + advanceButton.disabled = false; + retractButton.disabled = false; + cursorButton.disabled = false; + bottomButton.disabled = false; +} + +function is_defined(x) +{ + return (typeof x != "undefined"); +} + +/* servicename: name of the service being called + * reqbody: text of the request + * processResponse: processes the server response + * (takes the response text in input, undefined in case of error) + */ +function callServer(servicename,processResponse,reqbody) +{ + 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; + + if(rs == 4) + { + stat = req.status; + stxt = req.statusText; + if(stat == 200) + { + processResponse(req.responseText); + } else { + processResponse(); + } + // resume(); + } + }; + req.open("POST", servicename); // + escape(unlocked.innerHTML), true); + if (reqbody) { + req.send(reqbody); + } else { + req.send(); + } + +} + +function advanceForm1() +{ + processor = function(responseText) { + if (is_defined(responseText)) { + // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); + response = 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; + metasenv = response[1]; + populate_goalarray(response[1]); + statements = listcons(len2,statements); + unlocked.scrollIntoView(true); + } else { + debug("advance failed"); + } + resume(); + }; + pause(); + callServer("advance",processor,unlocked.innerHTML.unescapeHTML()); + +} + +function gotoBottom() +{ + processor = function(responseText) { + if (is_defined(responseText)) { + // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND"); + response = 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 failed"); + } + resume(); + }; + pause(); + callServer("bottom",processor,unlocked.innerHTML.unescapeHTML()); + +} + + +function gotoPos(offset) +{ + if (!is_defined(offset)) { + offset = getCursorPos(); + } + processor = function(responseText) { + if (is_defined(responseText)) { + // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); + response = 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; + statements = listcons(len2,statements); + metasenv = response[1]; + // la populate non andrebbe fatta a ogni passo + if (offset <= len) { + populate_goalarray(response[1]); + resume(); + } else { + gotoPos(offset - len); + } + } else { + unlocked.scrollIntoView(true); + populate_goalarray(metasenv); + resume(); + } + } + pause(); + callServer("advance",processor,unlocked.innerHTML.unescapeHTML()); +} + +function retract() +{ + processor = function(responseText) { + if (typeof responseText != "undefined") { + debug("retract: received response\nBEGIN\n" + responseText + "\nEND"); + 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(responseText); + unlocked.scrollIntoView(true); + } else { + debug("retract failed"); + } + resume(); + }; + debug("retract 1"); + pause(); + callServer("retract",processor); + debug("retract 2"); +} + +function openFile() +{ + processor = function(responseText) + { + if (responseText) { + locked.innerHTML = ""; + unlocked.innerHTML = responseText; + } else { + debug("file open failed"); + } + }; + callServer("open?file=" + escape(filename.value),processor); +} + +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); + } +} + +function findNode(list, node, acc) { + for (var i = 0; i < list.length; i++) { + if (list[i] == node) { + // debug("success " + i); + return acc; + } + if (list[i].hasChildNodes()) { + try { + // debug("recursion on node " + i); + return (findNode(list[i].childNodes,node,acc)) + } + catch (e) { /* debug("recursion failed"); */ } + } + sandbox = document.getElementById("sandbox"); + dup = list[i].cloneNode(true); + sandbox.appendChild(dup); +// debug("fail " + i + ": " + sandbox.innerHTML); + acc += sandbox.innerHTML.length; + sandbox.removeChild(dup); + } + throw "not found"; +} + +function test () { + debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos())); +}