From a7b54fb6f31e5ac626853890686ee54033dc7b24 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 18 Oct 2011 15:41:04 +0000 Subject: [PATCH] Localization of errors. --- matitaB/matita/matitadaemon.ml | 51 ++++++++++++++++++++------- matitaB/matita/matitaweb.css | 6 ++++ matitaB/matita/matitaweb.js | 64 +++++++++++++++++++++++++--------- 3 files changed, 92 insertions(+), 29 deletions(-) diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 606ccea4a..c92811c4e 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -1,6 +1,8 @@ open Printf;; open Http_types;; +exception Emphasized_error of string + module Stack = Continuationals.Stack let rt_path () = Helm_registry.get "matita.rt_base_dir" @@ -29,9 +31,13 @@ let do_global_commit () = let ft = MatitaAuthentication.read_ft u in (* first we add new files/dirs to the repository *) - let to_be_added = List.map fst - (List.filter (fun (_,flag) -> flag = MatitaFilesystem.MAdd) ft) + (* must take the reverse because svn requires the add to be performed in + the correct order + (otherwise run with --parents option) *) + let to_be_added = List.rev (List.map fst + (List.filter (fun (_,flag) -> flag = MatitaFilesystem.MAdd) ft)) in + prerr_endline ("@@@ ADDING files: " ^ String.concat ", " to_be_added); let out = try let newout = MatitaFilesystem.add_files u to_be_added in @@ -120,7 +126,10 @@ let do_global_commit () = (String.concat ", " not_added) (String.concat ", " not_committed) (String.concat ", " conflicts))) - "" (List.rev !to_be_committed) + (* XXX: at the moment, we don't keep track of the order in which users have + scheduled their commits, but we should, otherwise we will get a + "first come, random served" policy *) + "" (* (List.rev !to_be_committed) *) (MatitaAuthentication.get_users ()) ;; (*** from matitaScript.ml ***) @@ -337,12 +346,24 @@ let advance0 sid text = let status = MatitaAuthentication.get_status sid in let status = status#reset_disambiguate_db () in let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len = - try - eval_statement !include_paths (*buffer*) status (`Raw text) - with - | HExtlib.Localized (_,e) -> raise e - (*| End_of_file -> raise Margin *) - in + try + eval_statement !include_paths (*buffer*) status (`Raw text) + with + | HExtlib.Localized (floc,e) as exn -> + let x, y = HExtlib.loc_of_floc floc in + let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in + let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in + let post = Netconversion.ustring_sub `Enc_utf8 y + (Netconversion.ustring_length `Enc_utf8 text - y) text in + let _,title = MatitaExcPp.to_string exn in + (* let title = "" in *) + let marked = + pre ^ "\005span class=\"error\" title=\"" ^ title ^ "\"\006" ^ err ^ "\005/span\006" ^ post in + let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false + () (html_of_matita marked) in + raise (Emphasized_error marked) + (* | End_of_file -> ... *) + in let stringbuf = Ulexing.from_utf8_string new_statements in let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in let outstr = ref "" in @@ -480,8 +501,6 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (* prerr_endline ("serializing proof objects..."); *) GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string status#baseuri) status; - (* prerr_endline ("adding to the commit queue..."); *) - add_user_for_commit uid; (* prerr_endline ("done."); *) end; end; @@ -613,7 +632,15 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body - with + with + | Emphasized_error text -> +(* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> *) + let body = "" ^ text ^ " " in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string body | Not_found _ -> cgi # set_header ~status:`Internal_server_error diff --git a/matitaB/matita/matitaweb.css b/matitaB/matita/matitaweb.css index 03af7f6bb..9f0da2884 100644 --- a/matitaB/matita/matitaweb.css +++ b/matitaB/matita/matitaweb.css @@ -204,6 +204,12 @@ span.activegoal { font-weight: bold; } +span.error { + color:red; + text-decoration: none; + border-bottom: 2px dashed; +} + span.passivegoal { color: blue; } diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index f05639282..fedaaf7fb 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -33,6 +33,16 @@ function unescape_html(s) return text_of_html(u) } +function filterByClass (elements,class){ + var itemsfound = new Array; + for(var i=0;i