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)*$" *) let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script *) statement = let ast,unparsed_text = 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 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 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 let baseuri = status#baseuri in match script#bos, script#eos with | true, _ -> () | _, true -> GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) status | _ -> clean_current_baseuri status ;;*) let sequent_size = ref 40;; let include_paths = ref [];; (* * * ... * ... * * * ... * *) let output_status s = let _,_,metasenv,subst,_ = s#obj in let render_switch = function | Stack.Open i -> "?" ^ (string_of_int i) | Stack.Closed i -> "?" ^ (string_of_int i) ^ "" in let int_of_switch = function | Stack.Open i | Stack.Closed i -> i in let sequent = function | Stack.Open i -> let meta = List.assoc i metasenv in snd (ApplyTransformation.ntxt_of_cic_sequent ~metasenv ~subst ~map_unicode_to_tex:false !sequent_size s (i,meta)) | Stack.Closed _ -> "This goal has already been closed." in let render_sequent is_loc acc depth tag (pos,sw) = let metano = int_of_switch sw in let markup = if is_loc then (match depth, pos with | 0, 0 -> "" ^ (render_switch sw) ^ "" | 0, _ -> Printf.sprintf "|%d: %s" pos (render_switch sw) | 1, pos when Stack.head_tag s#stack = `BranchTag -> Printf.sprintf "|%d : %s" pos (render_switch sw) | _ -> render_switch sw) else render_switch sw in let markup = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () markup in let markup = "" ^ markup ^ "" in let sequent = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw) in let txt0 = "" ^ sequent ^ "" in "" ^ markup ^ txt0 ^ "" ^ acc in "" ^ (Stack.fold ~env:(render_sequent true) ~cont:(render_sequent false) ~todo:(render_sequent false) "" s#stack) ^ "" (* prerr_endline ("sending metasenv:\n" ^ res); res *) ;; let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";; let first_line s = let s = Pcre.replace ~rex:heading_nl_RE s in try let nl_pos = String.index s '\n' in String.sub s 0 nl_pos with Not_found -> s ;; let read_file fname = let chan = open_in fname in let lines = ref [] in (try while true do lines := input_line chan :: !lines done; with End_of_file -> close_in chan); String.concat "\n" (List.rev !lines) ;; let load_index outchan = let s = read_file "index.html" in Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan ;; let load_doc filename outchan = let s = read_file filename in let is_png = try String.sub filename (String.length filename - 4) 4 = ".png" with Invalid_argument _ -> false in let contenttype = if is_png then "image/png" else "text/html" in 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 env = cgi#environment in (try 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 (* cgi # set_header ~cache:`No_cache ~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 = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita (read_file filename)) in (* html_of_matita (read_file filename) in *) (* prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND"); *) let body = "" ^ body ^ "" in let baseuri, incpaths = try let root, baseuri, _fname, _tgt = Librarian.baseuri_of_script ~include_paths:[] filename in let includes = try Str.split (Str.regexp " ") (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) with Not_found -> [] in let rc = root :: includes in List.iter (HLog.debug) rc; baseuri, rc with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in include_paths := incpaths; 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 ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" ()); 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 = 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 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 assert (cgi#arguments <> []); let uid = cgi#argument_value "userid" in let userpw = cgi#argument_value "password" in (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 ("" ^ "Redirecting to login page...") with | MatitaAuthentication.UsernameCollision _ -> cgi#set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); cgi#out_channel#output_string "Error: User id collision!" | MatitaFilesystem.SvnError msg -> cgi#set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); cgi#out_channel#output_string ("

Error: Svn checkout failed!

")); 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 env = cgi#environment in assert (cgi#arguments <> []); let uid = cgi#argument_value "userid" in let userpw = cgi#argument_value "password" in (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"); 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 env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in MatitaAuthentication.logout_user sid; cgi # set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); let text = read_file (rt_path () ^ "/logout.html") in cgi#out_channel#output_string text with | Not_found _ -> cgi # set_header ~status:`Internal_server_error ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" ()); cgi#out_channel#commit_work() ;; 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 env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in let status = MatitaAuthentication.get_status sid in let uid = MatitaAuthentication.user_of_session sid in assert (cgi#arguments <> []); let locked = cgi#argument_value "locked" in let unlocked = cgi#argument_value "unlocked" in let dir = cgi#argument_value "dir" in 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) && already_exists) then raise File_already_exists; if dir = "true" then Unix.mkdir filename 0o744 else begin let oc = open_out filename in output_string oc (locked ^ unlocked); close_out oc; if MatitaEngine.eos status unlocked then begin (* prerr_endline ("serializing proof objects..."); *) GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string status#baseuri) status; (* prerr_endline ("done."); *) end; end; 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\"" (); 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 ~status:`Internal_server_error ~cache:`No_cache ~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() ;; 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 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 "" 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 ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" ()); 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 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 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); let details = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () details in MatitaAuthentication.set_file_flag uid files; 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 ("
" ^ 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 ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" ()); cgi#out_channel#commit_work() ;; (* 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 (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in (* cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); *) let text = cgi#argument_value "body" in (* prerr_endline ("body =\n" ^ text); *) let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in let txt = output_status new_status in let body = "" ^ new_parsed ^ "" ^ txt ^ "" in (* prerr_endline ("sending advance response:\n" ^ body); *) cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body 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 *) let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in 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 ((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; acc, error_msg e *) in (* cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); *) let text = cgi#argument_value "body" in (* prerr_endline ("body =\n" ^ text); *) 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 = "" ^ 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 ~cache:`No_cache ~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 env = cgi#environment in prerr_endline "executing goto Top"; (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in (* cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); *) let status = MatitaAuthentication.get_status sid in let uid = MatitaAuthentication.user_of_session sid in 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; *) 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; *) cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string "ok" with _ -> (cgi#set_header ~status:`Internal_server_error ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string "ok")); 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 env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in (* cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); *) 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 "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; MatitaAuthentication.set_status sid new_status; prerr_endline ("baseuri after retract = " ^ new_status#baseuri); let body = output_status new_status in cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body 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 env = cgi#environment in let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in (* cgi # set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); *) let uid = MatitaAuthentication.user_of_session sid in let ft = MatitaAuthentication.read_ft uid in let html = MatitaFilesystem.html_of_library uid ft in cgi # set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); cgi#out_channel#output_string ((* "\n" ^ "XML Tree Control\n" ^ "\n" ^ "\n" ^ "\n" ^ *) html (* ^ "\n" *) ); let files,anomalies = MatitaFilesystem.stat_user uid in let changed = HExtlib.filter_map (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 prerr_endline ("Changed:\n" ^ changed ^ "\n\nAnomalies:\n" ^ anomalies); cgi#out_channel#commit_work() ;; let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in MatitaAuthentication.reset (); cgi # set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); cgi#out_channel#output_string ("\n" ^ "Matitaweb Reset\n" ^ "

Reset completed

"); cgi#out_channel#commit_work() open Netcgi1_compat.Netcgi_types;; (**********************************************************************) (* Create the webserver *) (**********************************************************************) let start() = let (opt_list, cmdline_cfg) = Netplex_main.args() in let use_mt = ref true in let opt_list' = [ "-mt", Arg.Set use_mt, " Use multi-threading instead of multi-processing" ] @ opt_list in Arg.parse opt_list' (fun s -> raise (Arg.Bad ("Don't know what to do with: " ^ s))) "usage: netplex [options]"; let parallelizer = if !use_mt then Netplex_mt.mt() (* multi-threading *) else Netplex_mp.mp() in (* multi-processing *) (* let adder = { Nethttpd_services.dyn_handler = (fun _ -> process1); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in *) let do_advance = { Nethttpd_services.dyn_handler = (fun _ -> advance); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_retract = { Nethttpd_services.dyn_handler = (fun _ -> retract); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let goto_bottom = { Nethttpd_services.dyn_handler = (fun _ -> gotoBottom); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let goto_top = { Nethttpd_services.dyn_handler = (fun _ -> gotoTop); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let retrieve = { Nethttpd_services.dyn_handler = (fun _ -> retrieve); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_register = { Nethttpd_services.dyn_handler = (fun _ -> register); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_login = { Nethttpd_services.dyn_handler = (fun _ -> login); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_logout = { Nethttpd_services.dyn_handler = (fun _ -> logout); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_viewlib = { Nethttpd_services.dyn_handler = (fun _ -> viewLib); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_resetlib = { Nethttpd_services.dyn_handler = (fun _ -> resetLib); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_save = { Nethttpd_services.dyn_handler = (fun _ -> save); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_commit = { Nethttpd_services.dyn_handler = (fun _ -> initiate_commit); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_update = { Nethttpd_services.dyn_handler = (fun _ -> svn_update); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let nethttpd_factory = Nethttpd_plex.nethttpd_factory ~handlers:[ "advance", do_advance ; "retract", do_retract ; "bottom", goto_bottom ; "top", goto_top ; "open", retrieve ; "register", do_register ; "login", do_login ; "logout", do_logout ; "reset", do_resetlib ; "viewlib", do_viewlib ; "save", do_save ; "commit", do_commit ; "update", do_update] () in MatitaInit.initialize_all (); MatitaAuthentication.deserialize (); Netplex_main.startup parallelizer Netplex_log.logger_factories (* allow all built-in logging styles *) Netplex_workload.workload_manager_factories (* ... all ways of workload management *) [ nethttpd_factory ] (* make this nethttpd available *) cmdline_cfg ;; Sys.set_signal Sys.sigpipe Sys.Signal_ignore; start();;