From d2a3f16be6c74cc7d79198a6ed126103bb502aea Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 6 Jun 2011 14:55:54 +0000 Subject: [PATCH] This update uses XML for client-server communication. For unknown reasons, this doesn't seem to work well with Firefox (but works ok on Chrome). We reverted to a single process http daemon because of an annoying bug in Ocaml Http, causing the daemon to terminate randomly. --- matitaB/matita/matitadaemon.ml | 55 ++++++++++++----- matitaB/matita/matitaweb.js | 107 ++++++++++++++++++--------------- 2 files changed, 97 insertions(+), 65 deletions(-) diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 6601400ed..18caa7426 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -44,9 +44,14 @@ let history = ref [!status];; let include_paths = ["/home/barolo/matitaB/matita/lib"];; -(* lista [meta n., goal; meta n., goal; ... ] *) -(* "item1#item2#...#" *) - +(* + * + * ... + * ... + * + * + * ... + * *) let output_status s = let _,_,metasenv,subst,_ = s#obj in let render_switch = function @@ -68,7 +73,7 @@ let output_status s = let markup = if is_loc then (match depth, pos with - | 0, 0 -> "" ^ (render_switch sw) ^ " " + | 0, 0 -> "" ^ (render_switch sw) ^ "" | 0, _ -> Printf.sprintf "|%d: %s" pos (render_switch sw) | 1, pos when Stack.head_tag s#stack = `BranchTag -> @@ -76,13 +81,23 @@ let output_status s = | _ -> render_switch sw) else render_switch sw in - let markup = Netencoding.Url.encode ~plus:false markup in - let txt0 = Netencoding.Url.encode ~plus:false (sequent sw) in - (string_of_int metano ^ "|" ^ markup ^ "|" ^ txt0 ^ "#" ^ acc) + let markup = + Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () markup in + let markup = "" ^ markup ^ "" in + let sequent = + Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw) + in + let txt0 = "" ^ sequent ^ "" in + "" ^ markup ^ + txt0 ^ "" ^ acc in - Stack.fold - ~env:(render_sequent true) ~cont:(render_sequent false) - ~todo:(render_sequent false) "" s#stack + let res = "" ^ + (Stack.fold + ~env:(render_sequent true) ~cont:(render_sequent false) + ~todo:(render_sequent false) "" s#stack) ^ + "" + in + prerr_endline ("sending metasenv:\n" ^ res); res ;; (* let html_of_status s = @@ -226,7 +241,11 @@ let callback req outchan = prerr_endline "getting 'file' argument"; let filename = List.assoc "file" req#params_GET in prerr_endline ("reading file " ^ filename); - let body = read_file filename in + let body = + Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () + (read_file filename) in + prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND"); + let body = "" ^ body ^ "" in let _,baseuri,_,_ = Librarian.baseuri_of_script ~include_paths:[] filename in @@ -250,8 +269,11 @@ let callback req outchan = (0,"",txt), Printexc.to_string e, `Code 500) in (* prerr_endline ("server response:\n" ^ txt); *) - let body = (string_of_int parsed_len) ^ "@" ^ txt in - Http_daemon.respond ~code ~body outchan + let body = + "" ^ txt + ^ "" + in (prerr_endline ("sending advance response:\n" ^ body); + Http_daemon.respond ~code ~body outchan) | "/bottom" -> let script = req#body in prerr_endline ("body length = " ^ (string_of_int (String.length script))); @@ -270,8 +292,9 @@ let callback req outchan = (0,txt), Printexc.to_string e, `Code 500) in (* prerr_endline ("server response:\n" ^ txt); *) - let body = (string_of_int parsed_len) ^ "@" ^ txt in - Http_daemon.respond ~code ~body outchan + let body = + "" ^ txt + in Http_daemon.respond ~code ~body outchan | "/retract" -> (try let body = retract () in @@ -291,7 +314,7 @@ let spec = { Http_daemon.default_spec with callback = callback; port = 9999; - mode = `Thread; + mode = `Single (*`Thread *) ; } ;; diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 588643861..e87a19f52 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -149,31 +149,29 @@ function p33 (p) return (tripletmap (function (a,b,c) { return (c); }, p)); } -function populate_goalarray(txt) +function populate_goalarray(menv) { - if (txt == "") { + debug("metasenv.length = " + menv.length); + if (menv.length == 0) { 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); + for (i = 0; i < menv.length; i++) { + metano = menv[i].getAttribute("number"); + metaname = menv[i].childNodes[0].childNodes[0].data; + goal = menv[i].childNodes[1].childNodes[0].data; + debug ("found meta n. " + metano); + debug ("found goal\nBEGIN" + goal + "\nEND"); + goalarray[metano] = goal; + tmp_goallist = " " + metaname + "" + tmp_goallist; + metalist = listcons(metano,metalist); + debug ("goalarray[\"" + metano + "\"] = " + goalarray[metano]); + } goals.innerHTML = tmp_goallist; debug("new metalist is '" + metalist + "'"); if (is_nil(metalist)) { @@ -263,12 +261,22 @@ function callServer(servicename,processResponse,reqbody) stat = req.status; stxt = req.statusText; if(stat == 200) - { - processResponse(req.responseText); + { + debug(req.responseText); + if (window.DOMParser) { + parser=new DOMParser(); + xmlDoc=parser.parseFromString(req.responseText,"text/xml"); + } + else // Internet Explorer + { + xmlDoc=new ActiveXObject("Microsoft.XMLDOM"); + xmlDoc.async="false"; + xmlDoc.loadXML(req.responseText); + } + processResponse(xmlDoc); } else { - processResponse(); + processResponse(); } - // resume(); } }; req.open("POST", servicename); // + escape(unlocked.innerHTML), true); @@ -282,11 +290,10 @@ function callServer(servicename,processResponse,reqbody) function advanceForm1() { - processor = function(responseText) { - if (is_defined(responseText)) { + processor = function(xml) { + if (is_defined(xml)) { // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); - response = responseText.split("@"); - len = parseInt(response[0]); + len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length")); len0 = unlocked.innerHTML.length; unescaped = unlocked.innerHTML.unescapeHTML(); parsedtxt = unescaped.substr(0,len); @@ -295,8 +302,8 @@ function advanceForm1() unlocked.innerHTML = unparsedtxt; len1 = unlocked.innerHTML.length; len2 = len0 - len1; - metasenv = response[1]; - populate_goalarray(response[1]); + metasenv = xml.getElementsByTagName("meta"); + populate_goalarray(metasenv); statements = listcons(len2,statements); unlocked.scrollIntoView(true); } else { @@ -311,22 +318,22 @@ function advanceForm1() function gotoBottom() { - processor = function(responseText) { - if (is_defined(responseText)) { + processor = function(xml) { + if (is_defined(xml)) { // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND"); - response = responseText.split("@"); - len = parseInt(response[0]); - len0 = unlocked.innerHTML.length; + len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length")); + 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); + len2 = len0 - len1; + metasenv = xml.getElementsByTagName("meta"); + populate_goalarray(metasenv); + statements = listcons(len2,statements); + unlocked.scrollIntoView(true); } else { debug("goto bottom failed"); } @@ -343,11 +350,10 @@ 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]); + processor = function(xml) { + if (is_defined(xml)) { + // debug("goto pos: received response\nBEGIN\n" + req.responseText + "\nEND"); + len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length")); len0 = unlocked.innerHTML.length; unescaped = unlocked.innerHTML.unescapeHTML(); parsedtxt = unescaped.substr(0,len); @@ -356,11 +362,13 @@ function gotoPos(offset) unlocked.innerHTML = unparsedtxt; len1 = unlocked.innerHTML.length; len2 = len0 - len1; + metasenv = xml.getElementsByTagName("meta"); + // populate_goalarray(metasenv); statements = listcons(len2,statements); - metasenv = response[1]; + unlocked.scrollIntoView(true); // la populate non andrebbe fatta a ogni passo if (offset <= len) { - populate_goalarray(response[1]); + populate_goalarray(metasenv); resume(); } else { gotoPos(offset - len); @@ -377,16 +385,17 @@ function gotoPos(offset) function retract() { - processor = function(responseText) { - if (typeof responseText != "undefined") { - debug("retract: received response\nBEGIN\n" + responseText + "\nEND"); + processor = function(xml) { + if (typeof xml != "undefined") { + // debug("advance: received response\nBEGIN\n" + req.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); + metasenv = xml.getElementsByTagName("meta"); + populate_goalarray(metasenv); unlocked.scrollIntoView(true); } else { debug("retract failed"); @@ -401,11 +410,11 @@ function retract() function openFile() { - processor = function(responseText) + processor = function(xml) { - if (responseText) { + if (is_defined(xml)) { locked.innerHTML = ""; - unlocked.innerHTML = responseText; + unlocked.innerHTML = xml.documentElement.firstChild.data; } else { debug("file open failed"); } -- 2.39.2