X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=fc8c9684e87534819f855ba1786723c347738e2a;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=95ff43b17f852704fec42989414cda56a10cfca7;hpb=9ebdeda9a6446cbae517b5c577fe15b53db262dc;p=helm.git diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 95ff43b17..fc8c9684e 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -1,14 +1,159 @@ open Printf;; open Http_types;; +exception Emphasized_error of string +exception Disamb_error of string +exception Generic_error of string + module Stack = Continuationals.Stack +let debug = prerr_endline +(* disable for debug *) +let prerr_endline _ = () + let rt_path () = Helm_registry.get "matita.rt_base_dir" let libdir uid = (rt_path ()) ^ "/users/" ^ uid let utf8_length = Netconversion.ustring_length `Enc_utf8 +let mutex = Mutex.create ();; + +let to_be_committed = ref [];; + +let html_of_matita s = + let patt1 = Str.regexp "\005" in + let patt2 = Str.regexp "\006" in + let patt3 = Str.regexp "<" in + let patt4 = Str.regexp ">" in + let res = Str.global_replace patt4 ">" s in + let res = Str.global_replace patt3 "<" res in + let res = Str.global_replace patt2 ">" res in + let res = Str.global_replace patt1 "<" res in + res +;; + +(* adds a user to the commit queue; concurrent instances possible, so we + * enclose the update in a CS + *) +let add_user_for_commit uid = + Mutex.lock mutex; + to_be_committed := uid::List.filter (fun x -> x <> uid) !to_be_committed; + Mutex.unlock mutex; +;; + +let do_global_commit (* () *) uid = + prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed); + List.fold_left + (fun out u -> + let ft = MatitaAuthentication.read_ft u in + + (* first we add new files/dirs to the repository *) + (* must take the reverse because svn requires the add to be performed in + the correct order + (otherwise run with --parents option) *) + let to_be_added = List.rev (List.map fst + (List.filter (fun (_,flag) -> flag = MatitaFilesystem.MAdd) ft)) + in + prerr_endline ("@@@ ADDING files: " ^ String.concat ", " to_be_added); + let out = + try + let newout = MatitaFilesystem.add_files u to_be_added in + out ^ "\n" ^ newout + with + | MatitaFilesystem.SvnError outstr -> + prerr_endline ("ADD OF " ^ u ^ "FAILED:" ^ outstr); + out + in + + (* now we update the local copy (to merge updates from other users) *) + let out = try + let files,anomalies,(added,conflict,del,upd,merged) = + MatitaFilesystem.update_user u + in + let anomalies = String.concat "\n" anomalies in + let details = Printf.sprintf + ("%d new files\n"^^ + "%d deleted files\n"^^ + "%d updated files\n"^^ + "%d merged files\n"^^ + "%d conflicting files\n\n" ^^ + "Anomalies:\n%s") added del upd merged conflict anomalies + in + prerr_endline ("update details:\n" ^ details); + MatitaAuthentication.set_file_flag u files; + out ^ "\n" ^ details + with + | MatitaFilesystem.SvnError outstr -> + prerr_endline ("UPDATE OF " ^ u ^ "FAILED:" ^ outstr); + out + in + + (* we re-read the file table after updating *) + let ft = MatitaAuthentication.read_ft u in + + (* finally we perform the real commit *) + let modified = (List.map fst + (List.filter (fun (_,flag) -> flag = MatitaFilesystem.MModified) ft)) + in + let to_be_committed = to_be_added @ modified + in + let out = try + let newout = MatitaFilesystem.commit u to_be_committed in + out ^ "\n" ^ newout + with + | MatitaFilesystem.SvnError outstr -> + prerr_endline ("COMMIT OF " ^ u ^ "FAILED:" ^ outstr); + out + in + + (* call stat to get the final status *) + let files, anomalies = MatitaFilesystem.stat_user u in + let added,not_added = List.fold_left + (fun (a_acc, na_acc) fname -> + if List.mem fname (List.map fst files) then + a_acc, fname::na_acc + else + fname::a_acc, na_acc) + ([],[]) to_be_added + in + let committed,not_committed = List.fold_left + (fun (c_acc, nc_acc) fname -> + if List.mem fname (List.map fst files) then + c_acc, fname::nc_acc + else + fname::c_acc, nc_acc) + ([],[]) modified + in + let conflicts = List.map fst (List.filter + (fun (_,f) -> f = Some MatitaFilesystem.MConflict) files) + in + MatitaAuthentication.set_file_flag u + (List.map (fun x -> x, Some MatitaFilesystem.MSynchronized) (added@committed)); + MatitaAuthentication.set_file_flag u files; + out ^ "\n\n" ^ (Printf.sprintf + ("COMMIT RESULTS for %s\n" ^^ + "==============\n" ^^ + "added and committed (%d of %d): %s\n" ^^ + "modified and committed (%d of %d): %s\n" ^^ + "not added: %s\n" ^^ + "not committed: %s\n" ^^ + "conflicts: %s\n") + u (List.length added) (List.length to_be_added) (String.concat ", " added) + (List.length committed) (List.length modified) (String.concat ", " committed) + (String.concat ", " not_added) + (String.concat ", " not_committed) (String.concat ", " conflicts))) + + (* XXX: at the moment, we don't keep track of the order in which users have + scheduled their commits, but we should, otherwise we will get a + "first come, random served" policy *) + "" (* (List.rev !to_be_committed) *) + (* replace [uid] to commit all users: + (MatitaAuthentication.get_users ()) + *) + [uid] +;; + (*** from matitaScript.ml ***) (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *) @@ -19,31 +164,109 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script match statement with | `Raw text -> (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *) + prerr_endline ("raw text = " ^ text); let strm = GrafiteParser.parsable_statement status (Ulexing.from_utf8_string text) in + prerr_endline "before get_ast"; let ast = MatitaEngine.get_ast status include_paths strm in + prerr_endline "after get_ast"; ast, text | `Ast (st, text) -> st, text in + + (* do we want to generate a trace? *) + let is_auto (l,a) = + not (List.mem_assoc "demod" a || List.mem_assoc "paramod" a || + List.mem_assoc "fast_paramod" a || List.assoc "depth" a = "1" || + l <> None) + in + + let get_param a param = + try + Some (param ^ "=" ^ List.assoc param a) + with Not_found -> None + in + let floc = match ast with | GrafiteAst.Executable (loc, _) | GrafiteAst.Comment (loc, _) -> loc in - let _,lend = HExtlib.loc_of_floc floc in + let lstart,lend = HExtlib.loc_of_floc floc in let parsed_text, _parsed_text_len = HExtlib.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in + let parsed_text_len = utf8_length parsed_text in let byte_parsed_text_len = String.length parsed_text in let unparsed_txt' = 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 = + let href r = + 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 ", " + (HExtlib.filter_map (function + | NotationPt.NRef r -> Some (href r) + | _ -> None) + trace) + in - let status = - MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast) - in - (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*) - utf8_length parsed_text + match ast with + | GrafiteAst.Executable (_, + GrafiteAst.NCommand (_, + GrafiteAst.NObj (loc, astobj,_))) -> + let objname = NotationPt.name_of_obj astobj in + let status = + MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast) + in + let new_parsed_text = Ulexing.from_utf8_string parsed_text in + let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in + let outstr = ref "" in + ignore (SmallLexer.mk_small_printer interpr outstr new_parsed_text); + let x, y = HExtlib.loc_of_floc floc in + let pre = Netconversion.ustring_sub `Enc_utf8 0 x !outstr in + let post = Netconversion.ustring_sub `Enc_utf8 x + (Netconversion.ustring_length `Enc_utf8 !outstr - x) !outstr in + outstr := Printf.sprintf + "%s\005img class=\"anchor\" src=\"icons/tick.png\" id=\"%s\" /\006%s" pre objname post; + prerr_endline ("baseuri after advance = " ^ status#baseuri); + (* prerr_endline ("parser output: " ^ !outstr); *) + (status,!outstr, unparsed_txt'),parsed_text_len + | GrafiteAst.Executable (_, + GrafiteAst.NTactic (_, + [GrafiteAst.NAuto (_, (l,a as auto_params))])) when is_auto auto_params + -> + let l = match l with + | None -> None + | Some (_,l') -> Some (List.map (fun x -> "",0,x) l') + in + let trace_ref = ref [] in + let status = NnAuto.auto_tac ~params:(l,a) ~trace_ref status in + let new_parsed_text = pre ^ (Printf.sprintf + "/\005span class='autotactic'\006%s\005span class='autotrace'\006 trace %s\005/span\006\005/span\006/" + (String.concat " " + (List.assoc "depth" a:: + HExtlib.filter_map (get_param a) ["width";"size"])) + (mk_univ !trace_ref)) + in + (status,new_parsed_text, unparsed_txt'),parsed_text_len + | _ -> + let status = + MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast) + in + let new_parsed_text = Ulexing.from_utf8_string parsed_text in + let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in + let outstr = ref "" in + ignore (SmallLexer.mk_small_printer interpr outstr new_parsed_text); + prerr_endline ("baseuri after advance = " ^ status#baseuri); + (* prerr_endline ("parser output: " ^ !outstr); *) + (status,!outstr, unparsed_txt'),parsed_text_len (*let save_moo status = let script = MatitaScript.current () in @@ -115,18 +338,6 @@ let output_status s = (* prerr_endline ("sending metasenv:\n" ^ res); res *) ;; -let html_of_matita s = - let patt1 = Str.regexp "\005" in - let patt2 = Str.regexp "\006" in - let patt3 = Str.regexp "<" in - let patt4 = Str.regexp ">" in - let res = Str.global_replace patt4 ">" s in - let res = Str.global_replace patt3 "<" res in - let res = Str.global_replace patt2 ">" res in - let res = Str.global_replace patt1 "<" res in - res -;; - let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";; let first_line s = @@ -176,6 +387,7 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~content_type:"text/xml; charset=\"utf-8\"" (); *) + let readonly = cgi # argument_value "readonly" in let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in (* prerr_endline ("reading file " ^ filename); *) let body = @@ -200,16 +412,23 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in include_paths := incpaths; - let status = (MatitaAuthentication.get_status sid)#set_baseuri baseuri in - let history = [status] in - MatitaAuthentication.set_status sid status; - MatitaAuthentication.set_history sid history; + if readonly <> "true" then + (let status = new MatitaEngine.status (Some uid) baseuri in + let history = [status] in + MatitaAuthentication.set_status sid status; + MatitaAuthentication.set_history sid history); cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body; with + | Sys_error _ -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string "" | Not_found _ -> cgi # set_header ~status:`Internal_server_error @@ -219,36 +438,178 @@ 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),(* newtext TODO *) _,parsed_len = - try - eval_statement !include_paths (*buffer*) status (`Raw text) - with - | HExtlib.Localized (_,e) -> raise e - (*| End_of_file -> raise Margin *) - in - let stringbuf = Ulexing.from_utf8_string new_statements in - let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in - let outstr = ref "" in - ignore (SmallLexer.mk_small_printer interpr outstr stringbuf); - prerr_endline ("baseuri after advance = " ^ st#baseuri); - (* prerr_endline ("parser output: " ^ !outstr); *) + let (st,new_statements,new_unparsed),parsed_len = + let rec do_exc = function + | MatitaEngine.EnrichedWithStatus (e,_) -> do_exc e + | NCicTypeChecker.TypeCheckerFailure s -> raise (Generic_error (Lazy.force s)) + | 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 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) + | 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 (s,Some exc) as e -> + prerr_endline + ("NTacStatus.Error " ^ Lazy.force s ^ " -- " ^ (Printexc.to_string exc)); + do_exc exc + | GrafiteDisambiguate.Ambiguous_input (loc,choices) -> + let x,y = HExtlib.loc_of_floc loc in + let choice_of_alias = function + | GrafiteAst.Ident_alias (_,uri) -> uri, None, uri + | GrafiteAst.Number_alias (None,desc) + | GrafiteAst.Symbol_alias (_,None,desc) -> "cic:/fakeuri.def(1)", Some desc, desc + | GrafiteAst.Number_alias (Some uri,desc) + | GrafiteAst.Symbol_alias (_,Some uri,desc) -> uri, Some desc, desc + in + let tag_of_choice (uri,title,desc) = + match title with + | None -> Printf.sprintf "%s" + uri + (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc) + | Some t -> Printf.sprintf "%s" + uri + (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () t) + (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc) + in + let strchoices = + String.concat "\n" + (List.map (fun x -> tag_of_choice (choice_of_alias x)) choices) + in + prerr_endline (Printf.sprintf + "@@@ Ambiguous input at (%d,%d). Possible choices:\n\n%s\n\n@@@ End." + x y strchoices); + (* + 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 = "Disambiguation Error" 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 + *) + let strchoices = Printf.sprintf + "%s" x y strchoices + in raise (Disamb_error strchoices) + | GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l)) + (* | End_of_file -> ... *) + | e -> + (* prerr_endline ("matitadaemon *** Unhandled exception " ^ Printexc.to_string e); *) + prerr_endline ("matitadaemon *** Unhandled exception " ^ snd (MatitaExcPp.to_string e)); + raise e + in + + try + eval_statement !include_paths (*buffer*) status (`Raw text) + with e -> do_exc e + in + debug "BEGIN PRINTGRAMMAR"; + (*prerr_endline (Print_grammar.ebnf_of_term status);*) + (*let kwds = String.concat ", " status#get_kwds in + debug ("keywords = " ^ kwds );*) + debug "END PRINTGRAMMAR"; 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 !outstr), new_unparsed, st + () (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 env = cgi#environment in + 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 ("" @@ -279,34 +640,28 @@ 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; + 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) = @@ -349,12 +704,13 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let rel_filename = cgi # argument_value "file" in let filename = libdir uid ^ "/" ^ rel_filename in let force = bool_of_string (cgi#argument_value "force") in + let already_exists = Sys.file_exists filename in - if ((not force) && (Sys.file_exists filename)) then + if ((not force) && already_exists) then raise File_already_exists; if dir = "true" then - Unix.mkdir filename 0o744 + Unix.mkdir filename 0o744 else begin let oc = open_out filename in @@ -365,20 +721,32 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (* prerr_endline ("serializing proof objects..."); *) GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string status#baseuri) status; - (* prerr_endline ("adding to the commit queue..."); *) - MatitaFilesystem.add_user uid; (* prerr_endline ("done."); *) end; end; - MatitaAuthentication.set_file_flag uid - [rel_filename, Some MatitaFilesystem.MModified]; + let old_flag = + try + List.assoc rel_filename (MatitaAuthentication.read_ft uid) + with Not_found -> MatitaFilesystem.MUnversioned + in + (if old_flag <> MatitaFilesystem.MConflict && + old_flag <> MatitaFilesystem.MAdd then + let newflag = + if already_exists then MatitaFilesystem.MModified + else MatitaFilesystem.MAdd + in + MatitaAuthentication.set_file_flag uid [rel_filename, Some newflag]); cgi # set_header - ~cache:`No_cache - ~content_type:"text/xml; charset=\"utf-8\"" - (); + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); cgi#out_channel#output_string "ok" with | File_already_exists -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); cgi#out_channel#output_string "cancelled" | Sys_error _ -> cgi # set_header @@ -387,6 +755,10 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~content_type:"text/xml; charset=\"utf-8\"" () | e -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); let estr = Printexc.to_string e in cgi#out_channel#output_string ("" ^ estr ^ "")); cgi#out_channel#commit_work() @@ -396,16 +768,27 @@ 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 (try - let errors,out = MatitaFilesystem.do_global_commit () in + let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in + let sid = HExtlib.unopt sid in + MatitaAuthentication.probe_commit_priv sid; + let uid = MatitaAuthentication.user_of_session sid in + let out = do_global_commit (* () *) uid in cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string ""; cgi#out_channel#output_string "ok"; - cgi#out_channel#output_string "
" ^ out ^ "
"; + cgi#out_channel#output_string ("
" ^ out ^ "
"); cgi#out_channel#output_string "" with + | Failure _ -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string + "no commit privileges" | Not_found _ -> cgi # set_header ~status:`Internal_server_error @@ -422,6 +805,7 @@ let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = 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 @@ -448,6 +832,13 @@ let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#output_string ("
" ^ details ^ "
"); cgi#out_channel#output_string ""; with + | Failure _ -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string + "no commit privileges" | Not_found _ -> cgi # set_header ~status:`Internal_server_error @@ -459,6 +850,7 @@ 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 =*) let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in @@ -473,9 +865,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 = "" ^ @@ -488,38 +878,74 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body - with + with + | Generic_error text -> + let body = "" ^ text ^ "" in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string body + | Emphasized_error text -> +(* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> *) + let body = "" ^ text ^ "" in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string body + | Disamb_error text -> + let body = "" ^ text ^ "" in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string body + | End_of_file _ -> + let body = "" in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string body | Not_found _ -> cgi # set_header ~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 -> "" ^ 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 @@ -529,27 +955,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) = + "" ^ 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() ;; @@ -571,12 +997,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\"" @@ -593,7 +1019,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 (* @@ -603,13 +1029,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; @@ -621,7 +1052,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() @@ -659,7 +1092,7 @@ let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let files,anomalies = MatitaFilesystem.stat_user uid in let changed = HExtlib.filter_map - (fun (n,fl) -> if (List.mem MatitaFilesystem.Modified fl) then Some n else None) files + (fun (n,f) -> if (f = Some MatitaFilesystem.MModified) then Some n else None) files in let changed = String.concat "\n" changed in let anomalies = String.concat "\n" anomalies in