open Printf;; open Http_types;; exception Emphasized_error of string module Stack = Continuationals.Stack 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 [];; (* 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 () = 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) *) (MatitaAuthentication.get_users ()) ;; (*** 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; *) let strm = GrafiteParser.parsable_statement status (Ulexing.from_utf8_string text) in let ast = MatitaEngine.get_ast status include_paths strm in ast, text | `Ast (st, text) -> st, text in let floc = match ast with | GrafiteAst.Executable (loc, _) | GrafiteAst.Comment (loc, _) -> loc in let _,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 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 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 (*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 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 = 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 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; let status = (MatitaAuthentication.get_status sid)#set_baseuri 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 | 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 advance0 sid text = let status = MatitaAuthentication.get_status 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 (floc,e) as exn -> 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 = "" 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) | GrafiteDisambiguate.Ambiguous_input (loc,choices) -> let strchoices = String.concat "\n" (List.map GrafiteAst.description_of_alias choices) in let x,y = HExtlib.loc_of_floc loc 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 raise (Emphasized_error marked) (* | End_of_file -> ... *) 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); *) MatitaAuthentication.set_status sid st; parsed_len, Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita !outstr), 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 MatitaAuthentication.add_user uid userpw; (* 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 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 cgi#set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); cgi#out_channel#output_string "Authentication error" end; 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#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 -> 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 out = do_global_commit () 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 | 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 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 | 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 (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 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 = "" ^ 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 | 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 | 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 history = MatitaAuthentication.get_history sid in let rec aux parsed_len parsed_txt 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 -> 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 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 = aux 0 "" text in let status = MatitaAuthentication.get_status sid in let txt = output_status status in let body = "" ^ new_parsed ^ "" ^ txt ^ "" in (*let body = "" ^ txt ^ "" 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 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"); 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 _ -> 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();;