X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=081ce316538b6563bf38b55650cf1b13e7f458f2;hb=0d481cc22ba8ada5781885da5398086a0b5662f3;hp=14bcf1db6d9b757d34c50263f8fd26194cef33e3;hpb=99a272204b8840aa0e8aa29a64674f4516c5b561;p=helm.git
diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 14bcf1db6..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
@@ -401,6 +401,45 @@ 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 ""
+ x y (mk_alias a)
+ in
+
+ let mk_failure (il,loc,msg) =
+ let x,y = HExtlib.loc_of_floc loc in
+ Printf.sprintf "%s"
+ 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 -> "" ^ fl' ^ ""
+ | Some a -> Printf.sprintf "%s" (mk_alias a) fl'
+ in
+
+ let mk_located (loc,cl) =
+ let x,y = HExtlib.loc_of_floc loc in
+ Printf.sprintf "%s"
+ x y (String.concat "" (List.map mk_choice cl))
+ in
+ "" ^ (String.concat "" (List.map mk_located l)) ^ ""
+;;
+
let advance0 sid text =
let status = MatitaAuthentication.get_status sid in
let history = MatitaAuthentication.get_history sid in
@@ -473,7 +512,8 @@ let advance0 sid text =
*)
let strchoices = Printf.sprintf
"%s" 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;
@@ -521,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
- ("
"
- ^ "Redirecting to Matita page...")
- 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
+ (""
+ ^ "Redirecting to Matita page...")
+ with MatitaAuthentication.InvalidPassword ->
cgi#set_header
~cache:`No_cache
~content_type:"text/html; charset=\"utf-8\""
();
cgi#out_channel#output_string
- "Authentication error"
- end;
-
+ "Authentication error");
cgi#out_channel#commit_work()
-
;;
let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
@@ -746,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 = "" ^ text ^ "" in
cgi # set_header
~cache:`No_cache
@@ -773,7 +806,7 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
let error_msg = function
| Emphasized_error text -> "" ^ text ^ ""
- | Ambiguous text -> (* *) text
+ | Disamb_error text -> text
| End_of_file _ -> (* not an error *) ""
| e -> (* unmanaged error *)
"" ^