From: Wilmer Ricciotti Date: Tue, 7 Jun 2011 14:36:36 +0000 (+0000) Subject: Matitaweb daemon ported from Ocaml Http to Ocamlnet's Nethttpd X-Git-Tag: make_still_working~2456 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7f28a5e47bd10355fee4332fe77bbfcca15f39d6;p=helm.git Matitaweb daemon ported from Ocaml Http to Ocamlnet's Nethttpd --- diff --git a/matitaB/matita/.depend b/matitaB/matita/.depend index edf516bdc..75f3da02b 100644 --- a/matitaB/matita/.depend +++ b/matitaB/matita/.depend @@ -12,10 +12,8 @@ matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaEngine.cmi matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx -matitadaemon.cmo: matitaInit.cmi matitaGtkMisc.cmi matitaEngine.cmi \ - applyTransformation.cmi -matitadaemon.cmx: matitaInit.cmx matitaGtkMisc.cmx matitaEngine.cmx \ - applyTransformation.cmx +matitadaemon.cmo: matitaGtkMisc.cmi matitaEngine.cmi applyTransformation.cmi +matitadaemon.cmx: matitaGtkMisc.cmx matitaEngine.cmx applyTransformation.cmx matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi diff --git a/matitaB/matita/Makefile b/matitaB/matita/Makefile index 4f3bea4f7..8c3e8c29e 100644 --- a/matitaB/matita/Makefile +++ b/matitaB/matita/Makefile @@ -3,7 +3,7 @@ export SHELL=/bin/bash include ../Makefile.defs NULL = -H=@ +#H=@ ifeq ($(ANNOT),true) ANNOTOPTION = -dtypes @@ -15,6 +15,7 @@ OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) OCAMLDEP_FLAGS = -pp $(CAMLP5O) PKGS = -package "$(MATITA_REQUIRES)" CPKGS = -package "$(MATITA_CREQUIRES)" +WPKGS = -package "$(MATITA_WREQUIRES)" OCAML_THREADS_FLAGS = -thread OCAML_DEBUG_FLAGS = -g #OCAML_PROF=p -p a @@ -96,6 +97,8 @@ LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES)) CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_CREQUIRES)) CLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_CREQUIRES)) +WLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_WREQUIRES)) +WLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_WREQUIRES)) opt: $(PROGRAMS_OPT) $(NOINST_PROGRAMS_OPT) upx: $(PROGRAMS_UPX) .PHONY: opt upx @@ -121,7 +124,7 @@ linkonly: $(H)echo " OCAMLC matitac.ml" $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitac.ml $(H)echo " OCAMLC matitadaemon.ml" - $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitadaemon $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitadaemon.ml + $(H)$(OCAMLC) $(WPKGS) -linkpkg -o matitadaemon $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitadaemon.ml .PHONY: linkonly matita: matita.ml $(LIB_DEPS) $(CMOS) @@ -138,10 +141,10 @@ matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) $(H)echo " OCAMLOPT $<" $(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml -matitadaemon: matitadaemon.ml $(CLIB_DEPS) $(CMOS) $(MAINCMOS) +matitadaemon: matitadaemon.ml $(WLIB_DEPS) $(CMOS) $(MAINCMOS) $(H)echo " OCAMLC $<" - $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) $(MAINCMOS) matitadaemon.ml -matitadaemon.opt: matitadaemon.ml $(CLIBX_DEPS) $(CMXS) $(MAINCMXS) + $(H)$(OCAMLC) $(WPKGS) -linkpkg -o $@ $(CMOS) $(MAINCMOS) matitadaemon.ml +matitadaemon.opt: matitadaemon.ml $(WLIBX_DEPS) $(CMXS) $(MAINCMXS) $(H)echo " OCAMLOPT $<" $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) $(MAINCMXS) matitadaemon.ml diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 18caa7426..65ddaf2cc 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -3,6 +3,8 @@ open Http_types;; module Stack = Continuationals.Stack +let utf8_length = Netconversion.ustring_length `Enc_utf8 + (*** from matitaScript.ml ***) (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *) @@ -36,7 +38,8 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script let status = MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast) in - (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*) Glib.Utf8.length parsed_text + (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*) + utf8_length parsed_text let status = ref (new MatitaEngine.status "cic:/matita");; @@ -81,9 +84,11 @@ let output_status s = | _ -> render_switch sw) else render_switch sw in + prerr_endline "pippo1"; let markup = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () markup in let markup = "" ^ markup ^ "" in + prerr_endline "pippo2"; let sequent = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw) in @@ -114,20 +119,6 @@ let output_status s = String.concat "\n\n" txt ;; *) -(* returns the length of the executed text and an html representation of the - * current metasenv*) -let advance text (* (?bos=false) *) = - let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len = - (* try *) - eval_statement include_paths (*buffer*) !status (`Raw text) - (* with End_of_file -> raise Margin *) - in - status := st; - history := st :: !history; - let txt = output_status !status in - parsed_len, new_unparsed, txt -;; - let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";; let first_line s = @@ -138,33 +129,6 @@ let first_line s = with Not_found -> s ;; -let gotoBottom = - let rec aux parsed_len metasenv text = - try - prerr_endline ("evaluating: " ^ first_line text); - let plen,new_unparsed,cur_metasenv = advance text in - aux (parsed_len+plen) cur_metasenv new_unparsed - with - | End_of_file -> parsed_len, metasenv - | _ -> - prerr_endline ("goto bottom debug: metasenv = \n" ^ metasenv); - parsed_len, metasenv - in aux 0 "" -;; - -let retract () = - let new_history,new_status = - match !history with - _::(status::_ as history) -> - history, status - | [_] -> (prerr_endline "singleton";failwith "retract") - | _ -> (prerr_endline "nil"; assert false) in - NCicLibrary.time_travel !status; - history := new_history; - status := new_status; - output_status !status -;; - let read_file fname = let chan = open_in fname in let lines = ref [] in @@ -205,120 +169,186 @@ let call_service outchan = 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) +let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + let filename = cgi # argument_value "file" in + prerr_endline ("reading file " ^ filename); + let body = + Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () + (read_file filename) in + prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND"); + let body = "" ^ body ^ "" in + let _,baseuri,_,_ = + Librarian.baseuri_of_script ~include_paths:[] filename in - (* Http_daemon.respond ~code:(`Code 200) ~body: str outchan *) + status := (!status)#set_baseuri baseuri; + cgi#out_channel#output_string body; + cgi#out_channel#commit_work() +;; + +let advance0 text = + let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len = + (* try *) + eval_statement include_paths (*buffer*) !status (`Raw text) + (* with End_of_file -> raise Margin *) + in + status := st; + history := st :: !history; + parsed_len, new_unparsed - 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 = - Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () - (read_file filename) in - prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND"); - let body = "" ^ body ^ "" in - let _,baseuri,_,_ = - Librarian.baseuri_of_script ~include_paths:[] filename - 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 txt = output_status !status in - (0,"",txt), Printexc.to_string e, `Code 500) - in - (* prerr_endline ("server response:\n" ^ txt); *) - let body = - "" ^ txt - ^ "" - in (prerr_endline ("sending advance response:\n" ^ body); - Http_daemon.respond ~code ~body outchan) - | "/bottom" -> - let script = req#body in - prerr_endline ("body length = " ^ (string_of_int (String.length script))); - let (parsed_len,txt), res, code = - try gotoBottom 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 txt = output_status !status in - (0,txt), Printexc.to_string e, `Code 500) - in - (* prerr_endline ("server response:\n" ^ txt); *) - let body = - "" ^ txt - in Http_daemon.respond ~code ~body outchan - | "/retract" -> - (try - let body = retract () in - prerr_endline "retract OK"; - Http_daemon.respond ~code:(`Code 200) ~body outchan - with e -> - (prerr_endline (Printexc.to_string e); - Http_daemon.respond ~code:(`Code 500) outchan)) - | url -> - try - let url = String.sub url 1 (String.length url - 1) in - load_doc url outchan - with _ -> Http_daemon.respond_not_found ~url outchan +(* 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 + 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_unparsed = advance0 text in + let txt = output_status !status in + let body = + "" ^ txt + ^ "" + in + prerr_endline ("sending advance response:\n" ^ body); + cgi#out_channel#output_string body; + cgi#out_channel#commit_work() ;; -let spec = - { Http_daemon.default_spec with - callback = callback; - port = 9999; - mode = `Single (*`Thread *) ; - } +let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let rec aux parsed_len text = + try + prerr_endline ("evaluating: " ^ first_line text); + let plen,new_unparsed = advance0 text in + aux (parsed_len+plen) new_unparsed + with + | _ -> parsed_len + in + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi 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 = aux 0 text in + let txt = output_status !status in + let body = + "" ^ txt + ^ "" + in + prerr_endline ("sending goto bottom response:\n" ^ body); + cgi#out_channel#output_string body; + 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 + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + let new_history,new_status = + match !history with + _::(status::_ as history) -> + history, status + | [_] -> (prerr_endline "singleton";failwith "retract") + | _ -> (prerr_endline "nil"; assert false) in + NCicLibrary.time_travel !status; + history := new_history; + status := new_status; + let body = output_status !status in + cgi#out_channel#output_string body; + cgi#out_channel#commit_work() ;; -let _ = + +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 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 nethttpd_factory = + Nethttpd_plex.nethttpd_factory + ~handlers:[ "advance", do_advance + ; "retract", do_retract + ; "bottom", goto_bottom + ; "open", retrieve ] + () in MatitaInit.initialize_all (); - Http_daemon.main spec + 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();; diff --git a/matitaB/matita/matitaweb b/matitaB/matita/matitaweb new file mode 100755 index 000000000..8c52197bc --- /dev/null +++ b/matitaB/matita/matitaweb @@ -0,0 +1,2 @@ +#! +./matitadaemon -conf netplex.conf diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index e87a19f52..ecb0133c3 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -194,6 +194,19 @@ function switch_goal(meta) } } +String.prototype.sescape = function() { + var patt1 = /%/gi; + var patt2 = /=/gi; + var patt3 = /&/gi; + var patt4 = /\+/gi; + var result = this; + result = result.replace(patt1,"%25"); + result = result.replace(patt2,"%3D"); + result = result.replace(patt3,"%26"); + result = result.replace(patt4,"%2B"); + return (result); +} + String.prototype.unescapeHTML = function() { var patt1 = //gi; @@ -279,7 +292,8 @@ function callServer(servicename,processResponse,reqbody) } } }; - req.open("POST", servicename); // + escape(unlocked.innerHTML), true); + req.open("POST", servicename); // + escape(unlocked.innerHTML), true); + req.setRequestHeader("Content-type","application/x-www-form-urlencoded"); if (reqbody) { req.send(reqbody); } else { @@ -312,7 +326,7 @@ function advanceForm1() resume(); }; pause(); - callServer("advance",processor,unlocked.innerHTML.unescapeHTML()); + callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape()); } @@ -340,7 +354,7 @@ function gotoBottom() resume(); }; pause(); - callServer("bottom",processor,unlocked.innerHTML.unescapeHTML()); + callServer("bottom",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape()); } @@ -380,7 +394,7 @@ function gotoPos(offset) } } pause(); - callServer("advance",processor,unlocked.innerHTML.unescapeHTML()); + callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape()); } function retract() @@ -419,7 +433,7 @@ function openFile() debug("file open failed"); } }; - callServer("open?file=" + escape(filename.value),processor); + callServer("open",processor,"file=" + escape(filename.value)); } var goalcell; diff --git a/matitaB/matita/netplex.conf b/matitaB/matita/netplex.conf new file mode 100644 index 000000000..08b7481e6 --- /dev/null +++ b/matitaB/matita/netplex.conf @@ -0,0 +1,75 @@ +netplex { + controller { + max_level = "debug"; (* Log level *) + logging { + type = "stderr"; (* Log to stderr *) + } + }; + service { + name = "My HTTP file service"; + protocol { + (* This section creates the socket *) + name = "http"; + address { + type = "internet"; + bind = "0.0.0.0:9999"; (* Port 80 on all interfaces *) + }; + }; + processor { + (* This section specifies how to process data of the socket *) + type = "nethttpd"; + host { + (* Think of Apache's "virtual hosts" *) + pref_name = "localhost"; + pref_port = 9999; + names = "*:0"; (* Which requests are matched here: all *) + uri { + path = "/"; + service { + type = "file"; + docroot = "/home/barolo/matitaB/matita"; + media_types_file = "/etc/mime.types"; + enable_listings = true; + } + }; + uri { + path = "/open"; + service { + type = "dynamic"; + handler = "open"; + } + }; + uri { + path = "/advance"; + service { + type = "dynamic"; + handler = "advance"; + } + }; + uri { + path = "/retract"; + service { + type = "dynamic"; + handler = "retract"; + } + }; + uri { + path = "/bottom"; + service { + type = "dynamic"; + handler = "bottom"; + } + }; + }; + }; + workload_manager { + type = "dynamic"; + max_jobs_per_thread = 1; (* Everything else is senseless *) + min_free_jobs_capacity = 1; + max_free_jobs_capacity = 1; + max_threads = 20; + }; + } +} + +