From: matitaweb Date: Sun, 8 Jul 2012 07:19:18 +0000 (+0000) Subject: bug fixes X-Git-Tag: make_still_working~1615 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=31dccba27d8819bc5e4b9ad3fc6f244f4dfbfbc0;p=helm.git bug fixes --- diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js index 1b97b15cf..248eeaa67 100644 --- a/matitaB/matita/html/matitaweb.js +++ b/matitaB/matita/html/matitaweb.js @@ -262,9 +262,9 @@ function strip_tags(tagname,classname) { var tags; if (is_defined(classname)) { - tags = $(tagname + "." + classname); + tags = $("#unlocked " + tagname + "." + classname); } else { - tags = $(tagname); + tags = $("#unlocked " + tagname); } var tlen = tags.length; // preserving the value from removeChild operations for (i = 0; i < tlen; i++) { @@ -652,6 +652,7 @@ function advOneStep(xml) { var parsed = xml.getElementsByTagName("parsed")[0]; var ambiguity = xml.getElementsByTagName("ambiguity")[0]; var disamberr = xml.getElementsByTagName("disamberror")[0]; + var localized = xml.getElementsByTagName("localized")[0]; if (is_defined(parsed)) { // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); var len = parseInt(parsed.getAttribute("length")); @@ -743,12 +744,14 @@ function advOneStep(xml) { next_cp(0); } throw "Stop"; - } - else { - var error = xml.getElementsByTagName("error")[0]; - unlocked.innerHTML = error.childNodes[0].wholeText; - error(xml.childNodes[0].nodeValue); + } else if (is_defined(localized)) { + unlocked.innerHTML = localized.childNodes[0].wholeText; throw "Stop"; + } + else { + var err = xml.getElementsByTagName("error")[0]; + error(err.childNodes[0].nodeValue); + throw "Stop"; } } @@ -1381,7 +1384,9 @@ function newDialog() { callback = function (fname) { abortDialog("dialogBox"); - saveFile(fname,"","",false,newDialog,true); + saveFile(fname,"", + "(* new script *)", + false,newDialog,true); }; showLibrary("Create new file", callback, newDialog); } @@ -1437,6 +1442,7 @@ function createDir() { } else { alert("An error occurred :-("); } + resume(); dialogBox.reload(); }; pause(); diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index eba76597e..fc8c9684e 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -3,6 +3,7 @@ open Http_types;; exception Emphasized_error of string exception Disamb_error of string +exception Generic_error of string module Stack = Continuationals.Stack @@ -482,6 +483,8 @@ let advance0 sid text = let status = status#reset_disambiguate_db () in let (st,new_statements,new_unparsed),parsed_len = let rec do_exc = function + | MatitaEngine.EnrichedWithStatus (e,_) -> do_exc e + | NCicTypeChecker.TypeCheckerFailure s -> raise (Generic_error (Lazy.force s)) | HExtlib.Localized (floc,e) -> let x, y = HExtlib.loc_of_floc floc in let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in @@ -573,7 +576,8 @@ let advance0 sid text = | GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l)) (* | End_of_file -> ... *) | e -> - prerr_endline ("matitadaemon *** Unhandled exception " ^ Printexc.to_string e); + (* prerr_endline ("matitadaemon *** Unhandled exception " ^ Printexc.to_string e); *) + prerr_endline ("matitadaemon *** Unhandled exception " ^ snd (MatitaExcPp.to_string e)); raise e in @@ -596,7 +600,7 @@ let advance0 sid text = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita new_statements), new_unparsed, st -let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = +let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let _env = cgi#environment in @@ -629,7 +633,7 @@ let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; -let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = +let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in @@ -660,7 +664,7 @@ let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; -let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = +let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try @@ -685,7 +689,7 @@ let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = exception File_already_exists;; -let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = +let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try @@ -794,7 +798,7 @@ let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; -let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = +let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -875,9 +879,16 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (); cgi#out_channel#output_string body with + | Generic_error text -> + let body = "" ^ text ^ "" in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string body | Emphasized_error text -> (* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> *) - let body = "" ^ text ^ "" in + let body = "" ^ text ^ "" in cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" @@ -907,7 +918,7 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; -let gotoBottom (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 *) @@ -968,7 +979,7 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; -let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = +let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in prerr_endline "executing goto Top"; @@ -1005,7 +1016,7 @@ let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; -let retract (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 @@ -1050,7 +1061,7 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ;; -let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = +let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in @@ -1090,7 +1101,7 @@ let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ;; -let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = +let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in MatitaAuthentication.reset (); cgi # set_header