X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=a53d24f676ae3c3ec9a86e8182700e1a4aa9942c;hb=538cee79ad9754ad46015de1fd34a3ad808f08c7;hp=606ccea4a755878eced8b61addcab5a02a5c7668;hpb=6b526c6aededda450597abe1c65fb249ba6801aa;p=helm.git
diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 606ccea4a..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
@@ -120,7 +127,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 +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
@@ -480,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;
@@ -613,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