X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=058e797bb8af54bdbf9170cb6b8064f2d011fa27;hb=71c124b4f171059ec3d29d5e53079000773ec851;hp=95ff43b17f852704fec42989414cda56a10cfca7;hpb=9ebdeda9a6446cbae517b5c577fe15b53db262dc;p=helm.git

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 95ff43b17..058e797bb 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" 
@@ -9,6 +12,139 @@ let libdir uid = (rt_path ()) ^ "/users/" ^ uid
 
 let utf8_length = Netconversion.ustring_length `Enc_utf8
 
+let mutex = Mutex.create ();;
+
+let to_be_committed = ref [];;
+
+let html_of_matita s =
+  let patt1 = Str.regexp "\005" in
+  let patt2 = Str.regexp "\006" in
+  let patt3 = Str.regexp "<" in
+  let patt4 = Str.regexp ">" in
+  let res = Str.global_replace patt4 "&gt;" s in
+  let res = Str.global_replace patt3 "&lt;" res in
+  let res = Str.global_replace patt2 ">" res in
+  let res = Str.global_replace patt1 "<" res in
+  res
+;;
+
+(* adds a user to the commit queue; concurrent instances possible, so we
+ * enclose the update in a CS
+ *)
+let add_user_for_commit uid =
+  Mutex.lock mutex;
+  to_be_committed := uid::List.filter (fun x -> x <> uid) !to_be_committed;
+  Mutex.unlock mutex;
+;;
+
+let do_global_commit () =
+  prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed);
+  List.fold_left
+    (fun out u ->
+       let ft = MatitaAuthentication.read_ft u in
+
+       (* first we add new files/dirs to the repository *)
+       (* 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
+           out ^ "\n" ^ newout
+         with
+         | MatitaFilesystem.SvnError outstr -> 
+             prerr_endline ("ADD OF " ^ u ^ "FAILED:" ^ outstr);
+             out
+       in
+
+       (* now we update the local copy (to merge updates from other users) *)
+       let out = try
+         let files,anomalies,(added,conflict,del,upd,merged) = 
+           MatitaFilesystem.update_user u 
+         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);
+         MatitaAuthentication.set_file_flag u files;
+         out ^ "\n" ^ details 
+         with
+         | MatitaFilesystem.SvnError outstr -> 
+             prerr_endline ("UPDATE OF " ^ u ^ "FAILED:" ^ outstr);
+             out
+       in
+
+       (* we re-read the file table after updating *)
+       let ft = MatitaAuthentication.read_ft u in
+
+       (* finally we perform the real commit *)
+       let modified = (List.map fst
+         (List.filter (fun (_,flag) -> flag = MatitaFilesystem.MModified) ft))
+       in
+       let to_be_committed = to_be_added @ modified
+       in
+       let out = try
+         let newout = MatitaFilesystem.commit u to_be_committed in
+         out ^ "\n" ^ newout
+         with
+         | MatitaFilesystem.SvnError outstr -> 
+             prerr_endline ("COMMIT OF " ^ u ^ "FAILED:" ^ outstr);
+             out
+       in
+
+       (* call stat to get the final status *)
+       let files, anomalies = MatitaFilesystem.stat_user u in
+       let added,not_added = List.fold_left 
+         (fun (a_acc, na_acc) fname ->
+            if List.mem fname (List.map fst files) then
+               a_acc, fname::na_acc
+            else
+               fname::a_acc, na_acc)
+         ([],[]) to_be_added
+       in
+       let committed,not_committed = List.fold_left 
+         (fun (c_acc, nc_acc) fname ->
+            if List.mem fname (List.map fst files) then
+               c_acc, fname::nc_acc
+            else
+               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): %s\n" ^^
+         "modified and committed (%d of %d): %s\n" ^^
+         "not added: %s\n" ^^
+         "not committed: %s\n" ^^
+         "conflicts: %s\n")
+         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)))
+
+  (* 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 ***)
 (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)
 
@@ -19,31 +155,88 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script
     match statement with
     | `Raw text ->
         (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *)
+        prerr_endline ("raw text = " ^ text);
         let strm =
          GrafiteParser.parsable_statement status
           (Ulexing.from_utf8_string text) in
+        prerr_endline "before get_ast";
         let ast = MatitaEngine.get_ast status include_paths strm in
+        prerr_endline "after get_ast";
          ast, text
     | `Ast (st, text) -> st, text
   in
+
+  (* do we want to generate a trace? *)
+  let is_auto (l,a) = 
+    not (List.mem_assoc "demod" a || List.mem_assoc "paramod" a ||
+      List.mem_assoc "fast_paramod" a || List.assoc "depth" a = "1" ||
+      l <> None)
+  in
+
+  let get_param a param = 
+     try 
+       Some (param ^ "=" ^ List.assoc param a)
+     with Not_found -> None
+  in
+
   let floc = match ast with
   | GrafiteAst.Executable (loc, _)
   | GrafiteAst.Comment (loc, _) -> loc in
   
-  let _,lend = HExtlib.loc_of_floc floc in 
+  let lstart,lend = HExtlib.loc_of_floc floc in 
   let parsed_text, _parsed_text_len = 
     HExtlib.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
+  let parsed_text_len = utf8_length parsed_text in
   let byte_parsed_text_len = String.length parsed_text in
   let unparsed_txt' = 
     String.sub unparsed_text byte_parsed_text_len 
       (String.length unparsed_text - byte_parsed_text_len)
   in
+  let pre = Netconversion.ustring_sub `Enc_utf8  0 lstart parsed_text in
+
+  let mk_univ trace = 
+    let href r = 
+      Printf.sprintf "\005A href=\"%s\"\006%s\005/A\006"
+        (NReference.string_of_reference r) (NCicPp.r2s status true r)
+    in
+    if trace = [] then "{}"
+    else String.concat ", " 
+      (HExtlib.filter_map (function 
+        | NotationPt.NRef r -> Some (href r) 
+        | _ -> None)
+      trace)
+  in
   
-  let status = 
-    MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
-  in 
-  (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*)
-    utf8_length parsed_text
+  match ast with
+  | GrafiteAst.Executable (_,
+      GrafiteAst.NTactic (_,
+        [GrafiteAst.NAuto (_, (l,a as auto_params))])) when is_auto auto_params
+          ->
+          let l = match l with
+          | None -> None
+          | Some (_,l') -> Some (List.map (fun x -> "",0,x) l')
+          in
+          let trace_ref = ref [] in
+          let status = NnAuto.auto_tac ~params:(l,a) ~trace_ref status in
+          let new_parsed_text = pre ^ (Printf.sprintf 
+            "/\005span class='autotactic'\006%s\005span class='autotrace'\006 trace %s\005/span\006\005/span\006/"
+             (String.concat " " 
+               (List.assoc "depth" a::
+                HExtlib.filter_map (get_param a) ["width";"size"]))
+             (mk_univ !trace_ref))
+          in
+          (status,new_parsed_text, unparsed_txt'),parsed_text_len
+  | _ ->
+      let status = 
+        MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
+      in
+      let new_parsed_text = Ulexing.from_utf8_string parsed_text in
+      let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
+      let outstr = ref "" in
+      ignore (SmallLexer.mk_small_printer interpr outstr new_parsed_text);
+      prerr_endline ("baseuri after advance = " ^ status#baseuri);
+      (* prerr_endline ("parser output: " ^ !outstr); *)
+      (status,!outstr, unparsed_txt'),parsed_text_len
 
 (*let save_moo status = 
   let script = MatitaScript.current () in
@@ -115,18 +308,6 @@ let output_status s =
   (* prerr_endline ("sending metasenv:\n" ^ res); res *)
 ;;
 
-let html_of_matita s =
-  let patt1 = Str.regexp "\005" in
-  let patt2 = Str.regexp "\006" in
-  let patt3 = Str.regexp "<" in
-  let patt4 = Str.regexp ">" in
-  let res = Str.global_replace patt4 "&gt;" s in
-  let res = Str.global_replace patt3 "&lt;" res in
-  let res = Str.global_replace patt2 ">" res in
-  let res = Str.global_replace patt1 "<" res in
-  res
-;;
-
 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";;
 
 let first_line s =
@@ -221,28 +402,85 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 
 let advance0 sid text =
   let status = MatitaAuthentication.get_status sid in
+  let history = MatitaAuthentication.get_history 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
-  let stringbuf = Ulexing.from_utf8_string new_statements in
-  let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in
-  let outstr = ref "" in
-  ignore (SmallLexer.mk_small_printer interpr outstr stringbuf);
-  prerr_endline ("baseuri after advance = " ^ st#baseuri);
-  (* prerr_endline ("parser output: " ^ !outstr); *)
+  let (st,new_statements,new_unparsed),parsed_len =
+    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 "<choice href=\"%s\">%s</choice>"
+            uri 
+            (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
+        | Some t -> Printf.sprintf "<choice href=\"%s\" title=\"%s\">%s</choice>"
+            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
+        "<ambiguity start=\"%d\" stop=\"%d\">%s</ambiguity>" x y strchoices
+      in raise (Ambiguous strchoices) 
+   (* | End_of_file -> ...          *)
+  in
   MatitaAuthentication.set_status sid st;
+  MatitaAuthentication.set_history sid (st::history);
   parsed_len, 
     Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false 
-      () (html_of_matita !outstr), new_unparsed, st
+      () (html_of_matita new_statements), new_unparsed, st
 
 let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
-  let env = cgi#environment in
+  let _env = cgi#environment in
   
   assert (cgi#arguments <> []);
   let uid = cgi#argument_value "userid" in
@@ -349,12 +587,13 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
     let rel_filename = cgi # argument_value "file" in
     let filename = libdir uid ^ "/" ^ rel_filename in
     let force = bool_of_string (cgi#argument_value "force") in
+    let already_exists = Sys.file_exists filename in
 
-    if ((not force) && (Sys.file_exists filename)) then 
+    if ((not force) && already_exists) then 
       raise File_already_exists;
 
     if dir = "true" then
-      Unix.mkdir filename 0o744
+       Unix.mkdir filename 0o744
     else 
      begin
       let oc = open_out filename in
@@ -365,17 +604,25 @@ 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..."); *)
-        MatitaFilesystem.add_user uid;
         (* prerr_endline ("done."); *)
        end;
      end;
-    MatitaAuthentication.set_file_flag uid 
-      [rel_filename, Some MatitaFilesystem.MModified];
+    let old_flag =
+      try 
+        List.assoc rel_filename (MatitaAuthentication.read_ft uid)
+      with Not_found -> MatitaFilesystem.MUnversioned
+    in
+    (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]);
     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 "<response>ok</response>"
   with
   | File_already_exists ->
@@ -394,16 +641,16 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 
 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
+  let _env = cgi#environment in
   (try
-    let errors,out = MatitaFilesystem.do_global_commit () in
+    let out = do_global_commit () in
     cgi # set_header 
       ~cache:`No_cache 
       ~content_type:"text/xml; charset=\"utf-8\""
       ();
     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 ("<details>" ^ out ^ "</details>");
     cgi#out_channel#output_string "</commit>"
   with
   | Not_found _ -> 
@@ -473,9 +720,7 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
     *)
     let text = cgi#argument_value "body" in
     (* prerr_endline ("body =\n" ^ text); *)
-    let history = MatitaAuthentication.get_history sid in
     let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in
-    MatitaAuthentication.set_history sid (new_status::history);
     let txt = output_status new_status in
     let body = 
        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
@@ -488,7 +733,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 = "<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
+  | Ambiguous text ->
+    let body = "<response>" ^ text ^ "</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
@@ -501,25 +761,32 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 let gotoBottom (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 char_to_parse = cgi#a
+(*  (try  *)
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
     let sid = HExtlib.unopt sid in
     let history = MatitaAuthentication.get_history sid in
 
-    let rec aux parsed_len parsed_txt text =
+    let error_msg = function
+      | Emphasized_error text -> "<localized>" ^ text ^ "</localized>" 
+      | Ambiguous text -> (* <ambiguity> *) text
+      | End_of_file _ -> (* not an error *) ""
+      | e -> (* unmanaged error *)
+          "<error>" ^ 
+          (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () 
+            (Printexc.to_string e)) ^ "</error>"
+    in
+
+    let rec aux acc text =
       try
         prerr_endline ("evaluating: " ^ first_line text);
         let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in
-        aux (parsed_len+plen) (parsed_txt ^ new_parsed) new_unparsed
-      with 
-      | End_of_file -> 
+        aux ((plen,new_parsed)::acc) new_unparsed
+      with e -> 
           let status = MatitaAuthentication.get_status sid in
           GrafiteTypes.Serializer.serialize 
             ~baseuri:(NUri.uri_of_string status#baseuri) status;
-          if parsed_len > 0 then 
-            MatitaAuthentication.set_history sid (status::history);
-          parsed_len, parsed_txt
-      | _ -> parsed_len, parsed_txt
+          acc, error_msg e
     in
     (* 
     cgi # set_header 
@@ -529,27 +796,27 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
     *)
     let text = cgi#argument_value "body" in
     (* prerr_endline ("body =\n" ^ text); *)
-    let parsed_len, new_parsed = aux 0 "" text in
+    let len_parsedlist, err_msg = aux [] text in
     let status = MatitaAuthentication.get_status sid in
     let txt = output_status status in
+    let parsed_tag (len,txt) = 
+       "<parsed length=\"" ^ (string_of_int len) ^ "\">" ^ txt ^ "</parsed>"
+    in
+    (* List.rev: the list begins with the older parsed txt *)
     let body = 
-       "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
-       new_parsed ^ "</parsed>" ^ txt 
-       ^ "</response>"
-    in 
-    (*let body = 
-       "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt 
-       ^ "</response>"
-    in*) 
+       "<response>" ^
+       String.concat "" (List.rev (List.map parsed_tag len_parsedlist)) ^
+       txt ^ err_msg ^ "</response>"
+    in
     (* prerr_endline ("sending goto bottom response:\n" ^ body); *)
     cgi # set_header 
       ~cache:`No_cache 
       ~content_type:"text/xml; charset=\"utf-8\""
       ();
-    cgi#out_channel#output_string body
-   with Not_found -> cgi#set_header ~status:`Internal_server_error 
+    cgi#out_channel#output_string body;
+(*   with Not_found -> cgi#set_header ~status:`Internal_server_error 
       ~cache:`No_cache 
-      ~content_type:"text/xml; charset=\"utf-8\"" ());
+      ~content_type:"text/xml; charset=\"utf-8\"" ()); *)
   cgi#out_channel#commit_work() 
 ;;
 
@@ -593,7 +860,7 @@ let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   let env = cgi#environment in
-  (try 
+  (try  
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
     let sid = HExtlib.unopt sid in
     (*
@@ -659,7 +926,7 @@ let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
     
     let files,anomalies = MatitaFilesystem.stat_user uid in
     let changed = HExtlib.filter_map 
-      (fun (n,fl) -> if (List.mem MatitaFilesystem.Modified fl) then Some n else None) files
+      (fun (n,f) -> if (f = Some MatitaFilesystem.MModified) then Some n else None) files
     in
     let changed = String.concat "\n" changed in
     let anomalies = String.concat "\n" anomalies in