X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=081ce316538b6563bf38b55650cf1b13e7f458f2;hb=601adf4ee553a77be1c55bc29159ed0e209500a1;hp=20a1d91c97797cd8603078d677e016d45187148b;hpb=3b88d145e26b75f54ac6271a196c1ef315376123;p=helm.git diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 20a1d91c9..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,13 +401,52 @@ 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 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 @@ -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 @@ -758,7 +791,8 @@ 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() ;; @@ -772,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 *) "" ^ @@ -841,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\"" @@ -891,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()