X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=fc8c9684e87534819f855ba1786723c347738e2a;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=5c58db3713ab38f73bf7ccc5689dd89662ace5bc;hpb=2914bfbeac3c2e0f53ba8c612cd11b3b2afbabce;p=helm.git diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 5c58db371..fc8c9684e 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -1,6 +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)*$" *) @@ -11,76 +164,188 @@ 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 parsed_text, parsed_text_len = - MatitaGtkMisc.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) 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),"",(*parsed_text_len*) Glib.Utf8.length parsed_text - - -let status = ref (new MatitaEngine.status "cic:/matita");; - -let include_paths = ["/home/barolo/matitaB/matita/lib"];; - -let advance text (* (?bos=false) *) = - (* if bos then LibraryClean.clean_baseuris [self#buri_of_current_file]; - (* HLog.debug ("evaluating: " ^ first_line s ^ " ...");*) - let time1 = Unix.gettimeofday () in - let entries, newtext, parsed_len = *) - let (st,_),_,parsed_len = - (* try *) - eval_statement include_paths (*buffer*) !status (`Raw text) - (* with End_of_file -> raise Margin *) - in - status := st; - let _,_,metasenv,subst,_ = !status#obj in - let txt = List.fold_left - (fun acc (nmeta,_ as meta) -> - let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 () - (snd (ApplyTransformation.ntxt_of_cic_sequent - ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in - ("Goal ?" ^ (string_of_int nmeta) ^ "\n" ^ txt0)::acc) - [] metasenv - in - let txt = String.concat "\n\n" txt in - parsed_len, txt - (*in - let time2 = Unix.gettimeofday () in - HLog.debug ("... done in " ^ string_of_float (time2 -. time1) ^ "s"); - let new_statuses, new_statements = - let statuses, texts = List.split entries in - statuses, texts - in - history <- new_statuses @ history; - statements <- new_statements @ statements; - let start = buffer#get_iter_at_mark (`MARK locked_mark) in - let new_text = String.concat "" (List.rev new_statements) in - if statement <> None then - buffer#insert ~iter:start new_text - else begin - let parsed_text = String.sub s 0 parsed_len in - if new_text <> parsed_text then begin - let stop = start#copy#forward_chars (Glib.Utf8.length parsed_text) in - buffer#delete ~start ~stop; - buffer#insert ~iter:start new_text; - end; - end; - self#moveMark (Glib.Utf8.length new_text); - buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext*) + 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 = @@ -91,7 +356,7 @@ let read_file fname = lines := input_line chan :: !lines done; with End_of_file -> close_in chan); - String.concat "\r\n" (List.rev !lines) + String.concat "\n" (List.rev !lines) ;; let load_index outchan = @@ -99,105 +364,910 @@ let load_index outchan = Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan ;; -let call_service outchan = - try - (ignore(MatitaEngine.assert_ng - ~include_paths:["/home/barolo/matitaB/matita/lib"] (* ~outch:outchan *) - "/home/barolo/matitaB/matita/lib/basics/pts.ma"); - prerr_endline "fatto"; - let s = read_file "/home/barolo/matitaB/matita/lib/basics/pts.ma.mad" - 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 - e -> Http_daemon.respond ~code:(`Code 500) outchan -;; - -let callback req outchan = - let str = - (sprintf "request path = %s\n" req#path) ^ - (sprintf "request GET params = %s\n" - (String.concat ";" - (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_GET))) ^ - (sprintf "request POST params = %s\n" - (String.concat ";" - (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_POST))) ^ - (sprintf "request ALL params = %s\n" - (String.concat ";" - (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params))) ^ - (sprintf "cookies = %s\n" - (match req#cookies with - | None -> - "NO COOKIES " - ^ (if req#hasHeader ~name:"cookie" - then "('Cookie:' header was '" ^ req#header ~name:"cookie" ^ "')" - else "(No 'Cookie:' header received)") - | Some cookies -> - (String.concat ";" - (List.map (fun (n,v) -> String.concat "=" [n;v]) cookies)))) ^ - (sprintf "request BODY = '%s'\n\n" req#body) - in - (* Http_daemon.respond ~code:(`Code 200) ~body: str outchan *) - - prerr_endline str; - - match req#path with - | "/" -> load_index outchan - | "/matita" -> call_service outchan - | "/open" -> - prerr_endline "getting 'file' argument"; - let filename = List.assoc "file" req#params_GET in - prerr_endline ("reading file " ^ filename); - let body = read_file filename in - let _,baseuri,_,_ = - Librarian.baseuri_of_script ~include_paths:[] filename + | 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 - status := (!status)#set_baseuri baseuri; - Http_daemon.respond ~code:(`Code 200) ~body outchan - | "/advance" -> - let script = req#body in - prerr_endline ("body length = " ^ (string_of_int (String.length script))); - let (parsed_len,txt), res, code = - try advance script, "OK", `Code 200 - with - | HExtlib.Localized(_,e) - | e -> - (prerr_endline ("exception: " ^ Printexc.to_string e); - (try - NTacStatus.pp_tac_status !status - with e -> prerr_endline ("inner exception: " ^ - Printexc.to_string e)); - prerr_endline "end status"; - let _,_,metasenv,subst,_ = !status#obj in - let txt = List.fold_left - (fun acc (nmeta,_ as meta) -> - let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 () - (snd (ApplyTransformation.ntxt_of_cic_sequent - ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in - ("Goal ?" ^ (string_of_int nmeta) ^ "\n" ^ txt0)::acc) - [] metasenv - in - let txt = String.concat "\n\n" txt in - (0,txt), Printexc.to_string e, `Code 500) + let strchoices = + String.concat "\n" + (List.map (fun x -> tag_of_choice (choice_of_alias x)) choices) in - let txt = Netencoding.Url.encode ~plus:false txt in - let body = (string_of_int parsed_len) ^ "#" ^ txt in - Http_daemon.respond ~code ~body outchan - | url -> Http_daemon.respond_not_found ~url outchan + 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 spec = - { Http_daemon.default_spec with - callback = callback; - port = 9999; - mode = `Single; - } +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 _ = +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 (); - Http_daemon.main spec + 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();;