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

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 058e797bb..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,18 +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
@@ -469,7 +512,8 @@ 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;
@@ -517,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) =
@@ -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,14 +791,14 @@ 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
-  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
@@ -769,7 +806,7 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 
     let error_msg = function
       | Emphasized_error text -> "<localized>" ^ text ^ "</localized>" 
-      | Ambiguous text -> (* <ambiguity> *) text
+      | Disamb_error text -> text
       | End_of_file _ -> (* not an error *) ""
       | e -> (* unmanaged error *)
           "<error>" ^ 
@@ -838,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\""
@@ -888,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()