X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=081ce316538b6563bf38b55650cf1b13e7f458f2;hb=f5b9e1d5511a13ca5bb424c149781087aa0c8e31;hp=81fa956e1161b87855080b26a7882bb647c57b40;hpb=704bbf749f44396c1a610f336b4e1cf0d25e9370;p=helm.git

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 81fa956e1..081ce3165 100644
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -2,7 +2,7 @@ open Printf;;
 open Http_types;;
 
 exception Emphasized_error of string
-exception Ambiguous of string
+exception Disamb_error of string
 
 module Stack = Continuationals.Stack
 
@@ -192,6 +192,7 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script
     String.sub unparsed_text byte_parsed_text_len 
       (String.length unparsed_text - byte_parsed_text_len)
   in
+  prerr_endline (Printf.sprintf "ustring_sub caso 1: lstart=%d, parsed=%s" lstart parsed_text);
   let pre = Netconversion.ustring_sub `Enc_utf8  0 lstart parsed_text in
 
   let mk_univ trace = 
@@ -400,17 +401,60 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
+let xml_of_disamb_error l =
+  let mk_alias = function
+  | GrafiteAst.Ident_alias (_,uri) -> "href=\"" ^ uri ^ "\""
+  | GrafiteAst.Symbol_alias (_,uri,desc) 
+  | GrafiteAst.Number_alias (uri,desc) -> 
+      let uri = try HExtlib.unopt uri with _ -> "cic:/fakeuri.def(1)" in
+        "href=\"" ^ uri ^ "\" title=\"" ^ 
+        (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
+        ^ "\""
+  in
+
+  let mk_interpr (loc,a) =
+    let x,y = HExtlib.loc_of_floc loc in
+    Printf.sprintf "<interpretation start=\"%d\" stop=\"%d\" %s />"
+      x y (mk_alias a)
+  in
+
+  let mk_failure (il,loc,msg) =
+    let x,y = HExtlib.loc_of_floc loc in
+    Printf.sprintf "<failure start=\"%d\" stop=\"%d\" title=\"%s\">%s</failure>"
+      x y (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () msg)
+      (String.concat "" (List.map mk_interpr il))
+  in
+
+  let mk_choice (a,fl) = 
+    let fl' = String.concat "" (List.map mk_failure fl) in
+    match a with
+    | None -> "<choice>" ^ fl' ^ "</choice>"
+    | Some a -> Printf.sprintf "<choice %s>%s</choice>" (mk_alias a) fl'
+  in
+
+  let mk_located (loc,cl) =
+    let x,y = HExtlib.loc_of_floc loc in
+    Printf.sprintf "<choicepoint start=\"%d\" stop=\"%d\">%s</choicepoint>"
+      x y (String.concat "" (List.map mk_choice cl))
+  in
+  "<disamberror>" ^ (String.concat "" (List.map mk_located l)) ^ "</disamberror>"
+;;
+
 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
-    eval_statement !include_paths (*buffer*) status (`Raw text)
+      eval_statement !include_paths (*buffer*) status (`Raw text)
     with
     | HExtlib.Localized (floc,e) as exn ->
       let x, y = HExtlib.loc_of_floc floc in
+  prerr_endline (Printf.sprintf "ustring_sub caso 2: (%d,%d) parsed=%s" 0 x text);
       let pre = Netconversion.ustring_sub `Enc_utf8  0 x text in
+  prerr_endline (Printf.sprintf "ustring_sub caso 3: (%d,%d) parsed=%s" x (y-x) text);
       let err = Netconversion.ustring_sub `Enc_utf8  x (y-x) text in
+  prerr_endline (Printf.sprintf "ustring_sub caso 4: (%d,%d) parsed=%s" y (Netconversion.ustring_length `Enc_utf8 text - y) text);
       let post = Netconversion.ustring_sub `Enc_utf8 y 
          (Netconversion.ustring_length `Enc_utf8 text - y) text in
       let _,title = MatitaExcPp.to_string exn in
@@ -468,10 +512,12 @@ let advance0 sid text =
       *)
       let strchoices = Printf.sprintf
         "<ambiguity start=\"%d\" stop=\"%d\">%s</ambiguity>" x y strchoices
-      in raise (Ambiguous strchoices) 
+      in raise (Disamb_error strchoices)
+   | GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l))
    (* | 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
@@ -515,34 +561,27 @@ let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   assert (cgi#arguments <> []);
   let uid = cgi#argument_value "userid" in
   let userpw = cgi#argument_value "password" in
-  let pw,_ = MatitaAuthentication.lookup_user uid in
-
-  if pw = userpw then
-   begin
-   let ft = MatitaAuthentication.read_ft uid in
-   let _ = MatitaFilesystem.html_of_library uid ft in
-    let sid = MatitaAuthentication.create_session uid in
-    (* let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in
-       cgi#set_header ~set_cookies:[cookie] (); *)
-    env#set_output_header_field 
-      "Set-Cookie" ("session=" ^ (Uuidm.to_string sid));
-(*    env#set_output_header_field "Location" "/index.html" *)
-    cgi#out_channel#output_string
-     ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/index.html\">"
-     ^ "</head><body>Redirecting to Matita page...</body></html>")
-   end
-  else
-   begin
+  (try 
+      MatitaAuthentication.check_pw uid userpw;
+      let ft = MatitaAuthentication.read_ft uid in
+      let _ = MatitaFilesystem.html_of_library uid ft in
+       let sid = MatitaAuthentication.create_session uid in
+       (* let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in
+          cgi#set_header ~set_cookies:[cookie] (); *)
+       env#set_output_header_field 
+         "Set-Cookie" ("session=" ^ (Uuidm.to_string sid));
+   (*    env#set_output_header_field "Location" "/index.html" *)
+       cgi#out_channel#output_string
+        ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/index.html\">"
+        ^ "</head><body>Redirecting to Matita page...</body></html>")
+  with MatitaAuthentication.InvalidPassword ->
     cgi#set_header
       ~cache:`No_cache 
       ~content_type:"text/html; charset=\"utf-8\""
       ();
     cgi#out_channel#output_string
-      "<html><head></head><body>Authentication error</body></html>"
-   end;
-    
+      "<html><head></head><body>Authentication error</body></html>");
   cgi#out_channel#commit_work()
-  
 ;;
 
 let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
@@ -718,9 +757,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) ^ "\">" ^
@@ -742,7 +779,7 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
       ~content_type:"text/xml; charset=\"utf-8\""
       ();
     cgi#out_channel#output_string body
-  | Ambiguous text ->
+  | Disamb_error text -> 
     let body = "<response>" ^ text ^ "</response>" in 
     cgi # set_header 
       ~cache:`No_cache 
@@ -754,32 +791,39 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
       ~status:`Internal_server_error
       ~cache:`No_cache 
       ~content_type:"text/xml; charset=\"utf-8\""
-      ());
+      ()
+  );
   cgi#out_channel#commit_work()
 ;;
 
 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 
+(*  (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>" 
+      | Disamb_error text -> 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 +833,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() 
 ;;
 
@@ -831,12 +875,12 @@ let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
     let baseuri = status#baseuri in
     let new_status = new MatitaEngine.status (Some uid) baseuri in
     prerr_endline "gototop prima della time travel";
-    NCicLibrary.time_travel new_status;
+    (* NCicLibrary.time_travel new_status; *)
     prerr_endline "gototop dopo della time travel";
     let new_history = [new_status] in 
     MatitaAuthentication.set_history sid new_history;
     MatitaAuthentication.set_status sid new_status;
-    NCicLibrary.time_travel new_status;
+    (* NCicLibrary.time_travel new_status; *)
     cgi # set_header 
       ~cache:`No_cache 
       ~content_type:"text/xml; charset=\"utf-8\""
@@ -853,7 +897,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
     (*
@@ -881,7 +925,9 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
       ~content_type:"text/xml; charset=\"utf-8\""
       ();
     cgi#out_channel#output_string body
-   with _ -> cgi#set_header ~status:`Internal_server_error 
+   with e -> 
+    prerr_endline ("error in retract: " ^ Printexc.to_string e);
+    cgi#set_header ~status:`Internal_server_error 
       ~cache:`No_cache 
       ~content_type:"text/xml; charset=\"utf-8\"" ());
   cgi#out_channel#commit_work()