X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=a53d24f676ae3c3ec9a86e8182700e1a4aa9942c;hb=80e732607c2b96569ed7826bb2372bc8ace885db;hp=22debcda494e763a27affba238ef137276837a8b;hpb=21d29bf473dd0d89f555dc17e4f2b7b9b4ad6bd1;p=helm.git
diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 22debcda4..a53d24f67 100644
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -1,6 +1,9 @@
open Printf;;
open Http_types;;
+exception Emphasized_error of string
+exception Ambiguous of string
+
module Stack = Continuationals.Stack
let rt_path () = Helm_registry.get "matita.rt_base_dir"
@@ -29,9 +32,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
@@ -85,39 +92,45 @@ let do_global_commit () =
(* call stat to get the final status *)
let files, anomalies = MatitaFilesystem.stat_user u in
- let add_count,not_added = List.fold_left
- (fun (ac_acc, na_acc) fname ->
+ let added,not_added = List.fold_left
+ (fun (a_acc, na_acc) fname ->
if List.mem fname (List.map fst files) then
- ac_acc, fname::na_acc
+ a_acc, fname::na_acc
else
- ac_acc+1, na_acc)
- (0,[]) to_be_added
+ fname::a_acc, na_acc)
+ ([],[]) to_be_added
in
- let commit_count,not_committed = List.fold_left
- (fun (cc_acc, nc_acc) fname ->
+ let committed,not_committed = List.fold_left
+ (fun (c_acc, nc_acc) fname ->
if List.mem fname (List.map fst files) then
- cc_acc, fname::nc_acc
+ c_acc, fname::nc_acc
else
- cc_acc+1, nc_acc)
- (0,[]) modified
+ fname::c_acc, nc_acc)
+ ([],[]) modified
in
let conflicts = List.map fst (List.filter
(fun (_,f) -> f = Some MatitaFilesystem.MConflict) files)
in
+ MatitaAuthentication.set_file_flag u
+ (List.map (fun x -> x, Some MatitaFilesystem.MSynchronized) (added@committed));
MatitaAuthentication.set_file_flag u files;
out ^ "\n\n" ^ (Printf.sprintf
("COMMIT RESULTS for %s\n" ^^
"==============\n" ^^
- "added and committed: %d of %d\n" ^^
- "modified and committed: %d of %d\n" ^^
+ "added and committed (%d of %d): %s\n" ^^
+ "modified and committed (%d of %d): %s\n" ^^
"not added: %s\n" ^^
"not committed: %s\n" ^^
"conflicts: %s\n")
- u add_count (List.length to_be_added) commit_count
- (List.length modified) (String.concat ", " not_added)
+ u (List.length added) (List.length to_be_added) (String.concat ", " added)
+ (List.length committed) (List.length modified) (String.concat ", " committed)
+ (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 ***)
@@ -334,12 +347,73 @@ 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)
+ | NTacStatus.Error (s,None) as e ->
+ prerr_endline
+ ("NTacStatus.Error " ^ (Lazy.force s));
+ raise e
+ | NTacStatus.Error (s,Some exc) as e ->
+ prerr_endline
+ ("NTacStatus.Error " ^ Lazy.force s ^ " -- " ^ (Printexc.to_string exc));
+ raise e
+ | GrafiteDisambiguate.Ambiguous_input (loc,choices) ->
+ let x,y = HExtlib.loc_of_floc loc in
+ let choice_of_alias = function
+ | GrafiteAst.Ident_alias (_,uri) -> uri, None, uri
+ | GrafiteAst.Number_alias (None,desc)
+ | GrafiteAst.Symbol_alias (_,None,desc) -> "cic:/fakeuri.def(1)", Some desc, desc
+ | GrafiteAst.Number_alias (Some uri,desc)
+ | GrafiteAst.Symbol_alias (_,Some uri,desc) -> uri, Some desc, desc
+ in
+ let tag_of_choice (uri,title,desc) =
+ match title with
+ | None -> Printf.sprintf "%s"
+ uri
+ (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
+ | Some t -> Printf.sprintf "%s"
+ uri
+ (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () t)
+ (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
+ in
+ let strchoices =
+ String.concat "\n"
+ (List.map (fun x -> tag_of_choice (choice_of_alias x)) choices)
+ in
+ prerr_endline (Printf.sprintf
+ "@@@ Ambiguous input at (%d,%d). Possible choices:\n\n%s\n\n@@@ End."
+ x y strchoices);
+ (*
+ 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 = "Disambiguation Error" 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
+ *)
+ let strchoices = Printf.sprintf
+ "%s" x y strchoices
+ in raise (Ambiguous strchoices)
+ (* | 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
@@ -477,8 +551,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;
@@ -487,16 +559,17 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
List.assoc rel_filename (MatitaAuthentication.read_ft uid)
with Not_found -> MatitaFilesystem.MUnversioned
in
- if old_flag <> MatitaFilesystem.MConflict then
+ (if old_flag <> MatitaFilesystem.MConflict &&
+ old_flag <> MatitaFilesystem.MAdd then
let newflag =
if already_exists then MatitaFilesystem.MModified
else MatitaFilesystem.MAdd
in
- MatitaAuthentication.set_file_flag uid [rel_filename, Some newflag];
+ MatitaAuthentication.set_file_flag uid [rel_filename, Some newflag]);
cgi # set_header
- ~cache:`No_cache
- ~content_type:"text/xml; charset=\"utf-8\""
- ();
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
cgi#out_channel#output_string "ok"
with
| File_already_exists ->
@@ -609,7 +682,22 @@ 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
+ | Ambiguous text ->
+ 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