(* 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);
- ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\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
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 "<response>ok</response>"
+ cgi#out_channel#output_string "<commit>";
+ cgi#out_channel#output_string "<response>ok</response>";
+ cgi#out_channel#output_string "<details>" ^ out ^ "</details>";
+ cgi#out_channel#output_string "</commit>"
with
| Not_found _ ->
cgi # set_header
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 "<response>ok</response>"
+ cgi#out_channel#output_string "<update>";
+ cgi#out_channel#output_string "<response>ok</response>";
+ cgi#out_channel#output_string ("<details>" ^ details ^ "</details>");
+ cgi#out_channel#output_string "</update>";
with
| Not_found _ ->
cgi # set_header