From 71c124b4f171059ec3d29d5e53079000773ec851 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 15 Nov 2011 11:38:04 +0000 Subject: [PATCH] Matitaweb: goto bottom can now be undone step by step and also reports errors (basic error reporting as in advance). Should fix a problem with the status. --- matitaB/matita/matitadaemon.ml | 55 +++++++++-------- matitaB/matita/matitaweb.js | 108 +++++++++++++++++++++++++++------ 2 files changed, 120 insertions(+), 43 deletions(-) diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 81fa956e1..058e797bb 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -402,6 +402,7 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let advance0 sid text = let status = MatitaAuthentication.get_status sid in + let history = MatitaAuthentication.get_history sid in let status = status#reset_disambiguate_db () in let (st,new_statements,new_unparsed),parsed_len = try @@ -472,6 +473,7 @@ let advance0 sid text = (* | End_of_file -> ... *) in MatitaAuthentication.set_status sid st; + MatitaAuthentication.set_history sid (st::history); parsed_len, Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita new_statements), new_unparsed, st @@ -718,9 +720,7 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = *) let text = cgi#argument_value "body" in (* prerr_endline ("body =\n" ^ text); *) - let history = MatitaAuthentication.get_history sid in let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in - MatitaAuthentication.set_history sid (new_status::history); let txt = output_status new_status in let body = "" ^ @@ -761,25 +761,32 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in - (try + let char_to_parse = cgi#a +(* (try *) let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in let history = MatitaAuthentication.get_history sid in - let rec aux parsed_len parsed_txt text = + let error_msg = function + | Emphasized_error text -> "" ^ text ^ "" + | Ambiguous text -> (* *) text + | End_of_file _ -> (* not an error *) "" + | e -> (* unmanaged error *) + "" ^ + (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () + (Printexc.to_string e)) ^ "" + in + + let rec aux acc text = try prerr_endline ("evaluating: " ^ first_line text); let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in - aux (parsed_len+plen) (parsed_txt ^ new_parsed) new_unparsed - with - | (* End_of_file *) _ -> + aux ((plen,new_parsed)::acc) new_unparsed + with e -> let status = MatitaAuthentication.get_status sid in GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string status#baseuri) status; - if parsed_len > 0 then - MatitaAuthentication.set_history sid (status::history); - parsed_len, parsed_txt - (*| _ -> parsed_len, parsed_txt*) + acc, error_msg e in (* cgi # set_header @@ -789,27 +796,27 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = *) let text = cgi#argument_value "body" in (* prerr_endline ("body =\n" ^ text); *) - let parsed_len, new_parsed = aux 0 "" text in + let len_parsedlist, err_msg = aux [] text in let status = MatitaAuthentication.get_status sid in let txt = output_status status in + let parsed_tag (len,txt) = + "" ^ txt ^ "" + in + (* List.rev: the list begins with the older parsed txt *) let body = - "" ^ - new_parsed ^ "" ^ txt - ^ "" - in - (*let body = - "" ^ txt - ^ "" - in*) + "" ^ + String.concat "" (List.rev (List.map parsed_tag len_parsedlist)) ^ + txt ^ err_msg ^ "" + in (* prerr_endline ("sending goto bottom response:\n" ^ body); *) cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); - cgi#out_channel#output_string body - with Not_found -> cgi#set_header ~status:`Internal_server_error + cgi#out_channel#output_string body; +(* with Not_found -> cgi#set_header ~status:`Internal_server_error ~cache:`No_cache - ~content_type:"text/xml; charset=\"utf-8\"" ()); + ~content_type:"text/xml; charset=\"utf-8\"" ()); *) cgi#out_channel#commit_work() ;; @@ -853,7 +860,7 @@ let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in - (try + (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in (* diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index cd1e624e1..d1480e72d 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -317,6 +317,9 @@ function listnil() return (""); } +function list_append(l1,l2) +{ return (l1 + l2) } + function is_nil(l) { return (l == ""); @@ -588,7 +591,7 @@ function advanceForm1() var len = parseInt(parsed.getAttribute("length")); // len0 = unlocked.innerHTML.length; var unescaped = unlocked.innerHTML.html_to_matita(); - var parsedtxt = parsed.childNodes[0].nodeValue; + var parsedtxt = parsed.childNodes[0].wholeText; //parsedtxt = unescaped.substr(0,len); var unparsedtxt = unescaped.substr(len); lockedbackup += parsedtxt; @@ -665,7 +668,7 @@ function advanceForm1() } else { var error = xml.getElementsByTagName("error")[0]; - unlocked.innerHTML = error.childNodes[0].nodeValue; + unlocked.innerHTML = error.childNodes[0].wholeText; // debug(xml.childNodes[0].nodeValue); } } else { @@ -683,27 +686,95 @@ function gotoBottom() processor = function(xml) { if (is_defined(xml)) { // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND"); - parsed = xml.getElementsByTagName("parsed")[0]; - len = parseInt(parsed.getAttribute("length")); - if (len > 0) { + var parsed = xml.getElementsByTagName("parsed"); + var localized = xml.getElementsByTagName("localized")[0]; + var ambiguity = xml.getElementsByTagName("ambiguity")[0]; + var generic_err = xml.getElementsByTagName("error")[0]; + for (var i = 0;i < parsed.length; i++) { + var len = parsed[i].getAttribute("length"); // len0 = unlocked.innerHTML.length; - unescaped = unlocked.innerHTML.html_to_matita(); - // not working in mozilla - // parsedtxt = parsed.childNodes[0].nodeValue; - parsedtxt = parsed.childNodes[0].wholeText; + var unescaped = unlocked.innerHTML.html_to_matita(); + // the browser may decide to split textnodes: use wholeText! + var parsedtxt = parsed[i].childNodes[0].wholeText; //parsedtxt = unescaped.substr(0,len); - unparsedtxt = unescaped.substr(len); + var unparsedtxt = unescaped.substr(len); lockedbackup += parsedtxt; locked.innerHTML = lockedbackup; //.matita_to_html(); unlocked.innerHTML = unparsedtxt.matita_to_html(); // len1 = unlocked.innerHTML.length; - len2 = parsedtxt.length; - metasenv = xml.getElementsByTagName("meta"); - init_autotraces(); - populate_goalarray(metasenv); - if (len2 > 0) - statements = listcons(len2,statements); - unlocked.scrollIntoView(true); + var len2 = parsedtxt.length; + statements = listcons(len2,statements); + } + unlocked.scrollIntoView(true); + metasenv = xml.getElementsByTagName("meta"); + init_autotraces(); + populate_goalarray(metasenv); + + if (is_defined(ambiguity)) { + var start = parseInt(ambiguity.getAttribute("start")); + var stop = parseInt(ambiguity.getAttribute("stop")); + var choices = xml.getElementsByTagName("choice"); + + matita.ambiguityStart = start; + matita.ambiguityStop = stop; + matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); + matita.interpretations = []; + + var unlockedtxt = unlocked.innerHTML.html_to_matita(); + var pre = unlockedtxt.substring(0,start).matita_to_html(); + var mid = unlockedtxt.substring(start,stop).matita_to_html(); + var post = unlockedtxt.substring(stop).matita_to_html(); + unlocked.innerHTML = pre + + "" + + mid + "" + post; + + var title = "

Ambiguous input

"; + disambcell.innerHTML = title; + for (i = 0;i < choices.length;i++) { + matita.interpretations[i] = new Object(); + + var href = choices[i].getAttribute("href"); + var title = choices[i].getAttribute("title"); + var desc = choices[i].childNodes[0].nodeValue; + + matita.interpretations[i].href = href; + matita.interpretations[i].title = title; + matita.interpretations[i].desc = desc; + + var choice = document.createElement("input"); + choice.setAttribute("type","radio"); + choice.setAttribute("name","interpr"); + choice.setAttribute("href",href); + choice.setAttribute("title",title); + if (i == 0) choice.setAttribute("checked",""); + + disambcell.appendChild(choice); + disambcell.appendChild(document.createTextNode(desc)); + disambcell.appendChild(document.createElement("br")); + } + + var okbutton = document.createElement("input"); + okbutton.setAttribute("type","button"); + okbutton.setAttribute("value","OK"); + okbutton.setAttribute("onclick","do_disambiguate()"); + var cancelbutton = document.createElement("input"); + cancelbutton.setAttribute("type","button"); + cancelbutton.setAttribute("value","Cancel"); + cancelbutton.setAttribute("onclick","cancel_disambiguate()"); + + disambcell.appendChild(okbutton); + disambcell.appendChild(cancelbutton); + + disable_toparea(); + + matita.disambMode = true; + updateSide(); + } + if (is_defined(localized)) { + unlocked.innerHTML = localized.wholeText; + } + if (is_defined(generic_err)) { + debug("Unmanaged error:\n" ^ generic_err.wholeText); } } else { debug("goto bottom failed"); @@ -712,7 +783,6 @@ function gotoBottom() }; pause(); callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); - } @@ -757,7 +827,7 @@ function gotoPos(offset) len = parseInt(parsed.getAttribute("length")); // len0 = unlocked.innerHTML.length; unescaped = unlocked.innerHTML.html_to_matita(); - parsedtxt = parsed.childNodes[0].nodeValue; + parsedtxt = parsed.childNodes[0].wholeText; //parsedtxt = unescaped.substr(0,len); unparsedtxt = unescaped.substr(len); lockedbackup += parsedtxt; -- 2.39.2