From: matitaweb Date: Wed, 5 Oct 2011 10:44:08 +0000 (+0000) Subject: Matitaweb: several improvements to svn interface. X-Git-Tag: make_still_working~2236 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=9ebdeda9a6446cbae517b5c577fe15b53db262dc Matitaweb: several improvements to svn interface. Some cosmetic changes. --- diff --git a/matitaB/matita/icons/top.png b/matitaB/matita/icons/top.png new file mode 100644 index 000000000..37f93b466 Binary files /dev/null and b/matitaB/matita/icons/top.png differ diff --git a/matitaB/matita/matitaFilesystem.ml b/matitaB/matita/matitaFilesystem.ml index 637a997dc..13c40664b 100644 --- a/matitaB/matita/matitaFilesystem.ml +++ b/matitaB/matita/matitaFilesystem.ml @@ -103,6 +103,9 @@ let stat_classify line = | _ -> raise (SvnAnomaly line) in aux 0 [] +let count p l = + List.length (List.filter p l) + let stat_user user = let rt_dir = Helm_registry.get "matita.rt_base_dir" in let repo = Helm_registry.get "matita.weblib" in @@ -155,7 +158,7 @@ let checkout user = let repo = Helm_registry.get "matita.weblib" in let errno, outlines, errlines = exec_process - ("svn co " ^ repo ^ " " ^ rt_dir ^ "/users/" ^ user ^ "/") + ("svn co --non-interactive " ^ repo ^ " " ^ rt_dir ^ "/users/" ^ user ^ "/") in let files, anomalies = List.fold_left (fun (facc,eacc) line -> @@ -267,17 +270,27 @@ let update_user user = let repo = Helm_registry.get "matita.weblib" in let errno, outlines, errlines = exec_process - ("svn up " ^ rt_dir ^ "/users/" ^ user ^ "/ --non-interactive") + ("svn up --non-interactive " ^ rt_dir ^ "/users/" ^ user ^ "/") in let files, anomalies = List.fold_left (fun (facc,eacc) line -> try (let fname,flags = up_classify line user in - (fname,matita_flag_of_update flags)::facc), eacc + (fname, flags)::facc), eacc with | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines in - if errno = 0 then files, anomalies + let added = count (fun (_,flags) -> List.mem Add flags) files in + let conflict = count (fun (_,flags) -> List.mem Conflict flags) files in + let del = count (fun (_,flags) -> List.mem Delete flags) files in + let upd = count (fun (_,flags) -> List.mem Update flags) files in + let merged = count (fun (_,flags) -> List.mem Merge flags) files in + + let files = + List.map (fun (fname,flags) -> fname,matita_flag_of_update flags) files + in + + if errno = 0 then files, anomalies, (added,conflict,del,upd,merged) else raise (SvnError (string_of_output outlines errlines)) ;; @@ -289,22 +302,23 @@ let commit user = let repo = Helm_registry.get "matita.weblib" in let errno, outlines, errlines = exec_process - ("svn ci --message \"commit by user " ^ user ^ "\" " ^ rt_dir ^ "/users/" ^ user ^ "/") + ("svn ci --non-interactive --message \"commit by user " ^ user ^ "\" " ^ rt_dir ^ "/users/" ^ user ^ "/") in - if errno = 0 then () + if errno = 0 then + "BEGIN COMMIT - " ^ user ^ ":\n" ^ (string_of_output outlines errlines) ^ "END COMMIT - " ^ user ^ "\n\n" else raise (SvnError (string_of_output outlines errlines)) ;; let do_global_commit () = prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed); List.fold_left - (fun acc u -> + (fun (acc,out) u -> try - commit u; - acc + let newout = commit u in + acc, out ^ newout with | SvnError outstr -> - prerr_endline outstr; - u::acc) - [] (List.rev !to_be_committed) + prerr_endline ("COMMIT OF " ^ user ^ "FAILED:" ^ outstr); + u::acc,out) + ([],"") (List.rev !to_be_committed) ;; diff --git a/matitaB/matita/matitaFilesystem.mli b/matitaB/matita/matitaFilesystem.mli index 13d900bed..0347304ef 100644 --- a/matitaB/matita/matitaFilesystem.mli +++ b/matitaB/matita/matitaFilesystem.mli @@ -28,9 +28,11 @@ val reset_lib : unit -> unit val add_user : string -> unit -val do_global_commit : unit -> string list +val do_global_commit : unit -> string list * string -val update_user : string -> (string * matita_flag option) list * string list +val update_user : + string -> + (string * matita_flag option) list * string list * (int*int*int*int*int) val stat_user : string -> (string * svn_flag list) list * string list diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 0253eabc2..95ff43b17 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -115,20 +115,6 @@ let output_status s = (* prerr_endline ("sending metasenv:\n" ^ res); res *) ;; -(* let html_of_status s = - let _,_,metasenv,subst,_ = s#obj in - let txt = List.fold_left - (fun acc (nmeta,_ as meta) -> - let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent - ~metasenv ~subst ~map_unicode_to_tex:false 80 s meta) - in - prerr_endline ("### txt0 = " ^ txt0); - ("Goal ?" ^ (string_of_int nmeta) ^ "\n" ^ txt0)::acc) - [] metasenv - in - String.concat "\n\n" txt -;; *) - let html_of_matita s = let patt1 = Str.regexp "\005" in let patt2 = Str.regexp "\006" in @@ -410,13 +396,15 @@ let initiate_commit (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 errors = MatitaFilesystem.do_global_commit () in - prerr_endline ("commit errors: " ^ (String.concat " " errors)); + let errors,out = MatitaFilesystem.do_global_commit () in cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); - cgi#out_channel#output_string "ok" + cgi#out_channel#output_string ""; + cgi#out_channel#output_string "ok"; + cgi#out_channel#output_string "
" ^ out ^ "
"; + cgi#out_channel#output_string "" with | Not_found _ -> cgi # set_header @@ -434,19 +422,31 @@ let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let sid = HExtlib.unopt sid in let uid = MatitaAuthentication.user_of_session sid in (try - let files,anomalies = MatitaFilesystem.update_user uid in - (* let changed = HExtlib.filter_map - (fun (fl,n) -> if (List.mem MatitaFilesystem.Modified fl) then Some n else None) files - in - let changed = String.concat "\n" changed in - let anomalies = String.concat "\n" anomalies in - prerr_endline ("Changed:\n" ^ changed ^ "\n\nAnomalies:\n" ^ anomalies); *) + let files,anomalies,(added,conflict,del,upd,merged) = + MatitaFilesystem.update_user uid + in + let anomalies = String.concat "\n" anomalies in + let details = Printf.sprintf + ("%d new files\n"^^ + "%d deleted files\n"^^ + "%d updated files\n"^^ + "%d merged files\n"^^ + "%d conflicting files\n\n" ^^ + "Anomalies:\n%s") added del upd merged conflict anomalies + in + prerr_endline ("update details:\n" ^ details); + let details = + Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () details + in MatitaAuthentication.set_file_flag uid files; cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); - cgi#out_channel#output_string "ok" + cgi#out_channel#output_string ""; + cgi#out_channel#output_string "ok"; + cgi#out_channel#output_string ("
" ^ details ^ "
"); + cgi#out_channel#output_string ""; with | Not_found _ -> cgi # set_header diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 349097719..e4fbe5633 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -392,12 +392,14 @@ String.prototype.html_to_matita = function() var patt3 = />/gi var patt4 = /</gi; var patt5 = />/gi; + var patt6 = / /gi; var result = this; result = result.replace(patt1,"\n"); result = result.replace(patt2,"\005"); result = result.replace(patt3,"\006"); result = result.replace(patt4,"<"); result = result.replace(patt5,">"); + result = result.replace(patt6," "); return (unescape(result)); } @@ -695,7 +697,11 @@ function retrieveFile(thefile) // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue); // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue; debug(xml.childNodes[0].textContent); - unlocked.innerHTML = xml.childNodes[0].textContent; + if (document.all) { // IE + unlocked.innerHTML = xml.childNodes[0].text; + } else { + unlocked.innerHTML = xml.childNodes[0].textContent; + } } else { debug("file open failed"); @@ -870,9 +876,11 @@ function commitAll() { processor = function(xml) { if (is_defined(xml)) { - debug("commit succeeded(?)"); + debug(xml.getElementsByTagName("details")[0].textContent); + alert("Commit executed: see details in the log.\n\n" + + "NOTICE: this message does NOT imply (yet) that the commit was successful."); } else { - debug("commit failed!"); + alert("Commit failed!"); } resume(); }; @@ -884,9 +892,11 @@ function updateAll() { processor = function(xml) { if (is_defined(xml)) { - debug("update succeeded(?)"); + alert("Update executed.\n\n" + + "Details:\n" + + xml.getElementsByTagName("details")[0].textContent); } else { - debug("update failed!"); + alert("Update failed!"); } resume(); };