Matitaweb: goto bottom can now be undone step by step and also reports errors

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

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 81fa956e1161b87855080b26a7882bb647c57b40..058e797bb8af54bdbf9170cb6b8064f2d011fa27 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -402,6 +402,7 @@ 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),parsed_len =
     try
@@ -472,6 +473,7 @@ let advance0 sid text =
    (* | 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 new_statements), new_unparsed, st
@@ -718,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) ^ "\">" ^
@@ -761,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 
@@ -789,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() 
 ;;
 
@@ -853,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
     (*