Localization of errors.

[helm.git] / matitaB / matita / matitadaemon.ml

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 606ccea4a755878eced8b61addcab5a02a5c7668..c92811c4e6ea53e2eaa75aac97e793f58c8b50c7 100644 (file)
--- 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 = "<response><error>" ^ text ^ "</error> </response>" 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