X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=0c0f6cefda58da86b44c768b1d2d6c778d06004d;hb=b40e4e96e85103c7072985990c6b541371fd5a48;hp=81fa956e1161b87855080b26a7882bb647c57b40;hpb=704bbf749f44396c1a610f336b4e1cf0d25e9370;p=helm.git diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 81fa956e1..0c0f6cefd 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -2,10 +2,13 @@ open Printf;; open Http_types;; exception Emphasized_error of string -exception Ambiguous of string +exception Disamb_error of string module Stack = Continuationals.Stack +(* disable for debug *) +let prerr_endline _ = () + let rt_path () = Helm_registry.get "matita.rt_base_dir" let libdir uid = (rt_path ()) ^ "/users/" ^ uid @@ -192,6 +195,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 = @@ -199,8 +203,8 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script Printf.sprintf "\005A href=\"%s\"\006%s\005/A\006" (NReference.string_of_reference r) (NCicPp.r2s status true r) in - if trace = [] then "{}" - else String.concat ", " + (*if trace = [] then "{}" + else*) String.concat ", " (HExtlib.filter_map (function | NotationPt.NRef r -> Some (href r) | _ -> None) @@ -344,8 +348,7 @@ let load_doc filename outchan = Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan ;; -let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = - let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in +let retrieve (cgi : Netcgi.cgi_activation) = let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -400,34 +403,98 @@ 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) - with - | HExtlib.Localized (floc,e) as exn -> + let rec do_exc = function + | HExtlib.Localized (floc,e) -> let x, y = HExtlib.loc_of_floc floc in let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in let post = Netconversion.ustring_sub `Enc_utf8 y (Netconversion.ustring_length `Enc_utf8 text - y) text in - let _,title = MatitaExcPp.to_string exn in + let _,title = MatitaExcPp.to_string e in (* let title = "" in *) let marked = pre ^ "\005span class=\"error\" title=\"" ^ title ^ "\"\006" ^ err ^ "\005/span\006" ^ post in let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita marked) in - raise (Emphasized_error marked) + raise (Emphasized_error marked) + | Disambiguate.NoWellTypedInterpretation (floc,e) -> + let x, y = HExtlib.loc_of_floc floc in + let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in + let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in + let post = Netconversion.ustring_sub `Enc_utf8 y + (Netconversion.ustring_length `Enc_utf8 text - y) text in + (*let _,title = MatitaExcPp.to_string e in*) + (* let title = "" in *) + let marked = + pre ^ "\005span class=\"error\" title=\"" ^ e ^ "\"\006" ^ err ^ "\005/span\006" ^ post in + let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false + () (html_of_matita marked) in + raise (Emphasized_error marked) + | NCicRefiner.Uncertain m as exn -> + let floc, e = Lazy.force m in + let x, y = HExtlib.loc_of_floc floc in + let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in + let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in + let post = Netconversion.ustring_sub `Enc_utf8 y + (Netconversion.ustring_length `Enc_utf8 text - y) text in + (* let _,title = MatitaExcPp.to_string e in *) + (* let title = "" in *) + let marked = + pre ^ "\005span class=\"error\" title=\"" ^ e ^ "\"\006" ^ err ^ "\005/span\006" ^ post in + let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false + () (html_of_matita marked) in + raise (Emphasized_error marked) | NTacStatus.Error (s,None) as e -> prerr_endline - ("NTacStatus.Error " ^ (Lazy.force s)); - raise e + ("NTacStatus.Error " ^ (Lazy.force s)); raise e | NTacStatus.Error (s,Some exc) as e -> prerr_endline ("NTacStatus.Error " ^ Lazy.force s ^ " -- " ^ (Printexc.to_string exc)); - raise e + do_exc exc | GrafiteDisambiguate.Ambiguous_input (loc,choices) -> let x,y = HExtlib.loc_of_floc loc in let choice_of_alias = function @@ -468,23 +535,35 @@ 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 -> ... *) + | e -> raise e + in + + try + eval_statement !include_paths (*buffer*) status (`Raw text) + with e -> do_exc e in MatitaAuthentication.set_status sid st; + MatitaAuthentication.set_history sid (st::history); +(* prerr_endline "previous timestamp"; + status#print_timestamp(); + prerr_endline "current timestamp"; + st#print_timestamp(); *) parsed_len, Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita new_statements), new_unparsed, st -let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = - let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in +let register (cgi : Netcgi.cgi_activation) = let _env = cgi#environment in assert (cgi#arguments <> []); let uid = cgi#argument_value "userid" in let userpw = cgi#argument_value "password" in - (try - MatitaAuthentication.add_user uid userpw; + (try + (* currently registering only unprivileged users *) + MatitaAuthentication.add_user uid userpw false; (* env#set_output_header_field "Location" "/index.html" *) cgi#out_channel#output_string ("" @@ -508,45 +587,37 @@ let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; -let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = - let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in +let login (cgi : Netcgi.cgi_activation) = let env = cgi#environment in 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; + NCicLibrary.init (Some uid); + 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) = - let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in +let logout (cgi : Netcgi.cgi_activation) = let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -570,8 +641,7 @@ let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = exception File_already_exists;; -let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = - let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in +let save (cgi : Netcgi.cgi_activation) = let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -637,10 +707,12 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; -let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = - let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in - let _env = cgi#environment in +let initiate_commit (cgi : Netcgi.cgi_activation) = + let env = cgi#environment in (try + let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in + let sid = HExtlib.unopt sid in + MatitaAuthentication.probe_commit_priv sid; let out = do_global_commit () in cgi # set_header ~cache:`No_cache @@ -660,13 +732,13 @@ let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; -let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = - let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in +let svn_update (cgi : Netcgi.cgi_activation) = let env = cgi#environment in let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in let uid = MatitaAuthentication.user_of_session sid in (try + MatitaAuthentication.probe_commit_priv sid; let files,anomalies,(added,conflict,del,upd,merged) = MatitaFilesystem.update_user uid in @@ -704,8 +776,9 @@ let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (* returns the length of the executed text and an html representation of the * current metasenv*) -let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = - let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in +(*let advance =*) +let advance (cgi : Netcgi.cgi_activation) = + (* let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in *) let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -718,9 +791,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 = "" ^ @@ -742,7 +813,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 @@ -754,32 +825,38 @@ 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 gotoBottom (cgi : Netcgi.cgi_activation) = 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 -> "" ^ text ^ "" + | Disamb_error text -> text + | End_of_file _ -> (* not an error *) "" + | e -> (* unmanaged error *) + "" ^ + (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () + (Printexc.to_string e)) ^ "" + 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 -> acc, error_msg e + (* DON'T SERIALIZE NOW!!! 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,32 +866,31 @@ 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) = + "" ^ txt ^ "" + in + (* List.rev: the list begins with the older parsed txt *) let body = - "" ^ - new_parsed ^ "" ^ txt - ^ "" - in - (*let body = - "" ^ txt - ^ "" - in*) + "" ^ + String.concat "" (List.rev (List.map parsed_tag len_parsedlist)) ^ + txt ^ err_msg ^ "" + 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() ;; -let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = - let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in +let gotoTop (cgi : Netcgi.cgi_activation) = let env = cgi#environment in prerr_endline "executing goto Top"; (try @@ -831,12 +907,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\"" @@ -850,10 +926,9 @@ let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; -let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = - let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in +let retract (cgi : Netcgi.cgi_activation) = 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 (* @@ -863,13 +938,18 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (); *) let history = MatitaAuthentication.get_history sid in + let old_status = MatitaAuthentication.get_status sid in let new_history,new_status = match history with _::(status::_ as history) -> history, status | [_] -> (prerr_endline "singleton";failwith "retract") | _ -> (prerr_endline "nil"; assert false) in - prerr_endline ("prima della time travel"); +(* prerr_endline "timestamp prima della retract"; + old_status#print_timestamp (); + prerr_endline "timestamp della retract"; + new_status#print_timestamp (); + prerr_endline ("prima della time travel"); *) NCicLibrary.time_travel new_status; prerr_endline ("dopo della time travel"); MatitaAuthentication.set_history sid new_history; @@ -881,15 +961,16 @@ 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() ;; -let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = - let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in +let viewLib (cgi : Netcgi.cgi_activation) = let env = cgi#environment in let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -928,8 +1009,7 @@ let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ;; -let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = - let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in +let resetLib (cgi : Netcgi.cgi_activation) = MatitaAuthentication.reset (); cgi # set_header ~cache:`No_cache