4 module Stack = Continuationals.Stack
6 let utf8_length = Netconversion.ustring_length `Enc_utf8
8 let utf8_parsed_text s floc =
9 let start, stop = HExtlib.loc_of_floc floc in
10 let len = stop - start in
11 let res = Netconversion.ustring_sub `Enc_utf8 start len s in
12 res, String.length res
14 (*** from matitaScript.ml ***)
15 (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)
17 let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script *)
20 let ast,unparsed_text =
23 (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *)
25 GrafiteParser.parsable_statement status
26 (Ulexing.from_utf8_string text) in
27 let ast = MatitaEngine.get_ast status include_paths strm in
29 | `Ast (st, text) -> st, text
31 let floc = match ast with
32 | GrafiteAst.Executable (loc, _)
33 | GrafiteAst.Comment (loc, _) -> loc in
35 let _,lend = HExtlib.loc_of_floc floc in
36 let parsed_text, _parsed_text_len =
37 utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
38 let byte_parsed_text_len = String.length parsed_text in
40 String.sub unparsed_text byte_parsed_text_len
41 (String.length unparsed_text - byte_parsed_text_len)
45 MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
47 (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*)
48 utf8_length parsed_text
50 let sequent_size = ref 40;;
52 let include_paths = ref [];;
56 * <metaname>...</metaname>
63 let _,_,metasenv,subst,_ = s#obj in
64 let render_switch = function
65 | Stack.Open i -> "?" ^ (string_of_int i)
66 | Stack.Closed i -> "<S>?" ^ (string_of_int i) ^ "</S>"
68 let int_of_switch = function
69 | Stack.Open i | Stack.Closed i -> i
71 let sequent = function
73 let meta = List.assoc i metasenv in
74 snd (ApplyTransformation.ntxt_of_cic_sequent
75 ~metasenv ~subst ~map_unicode_to_tex:false !sequent_size s (i,meta))
76 | Stack.Closed _ -> "This goal has already been closed."
78 let render_sequent is_loc acc depth tag (pos,sw) =
79 let metano = int_of_switch sw in
82 (match depth, pos with
83 | 0, 0 -> "<B>" ^ (render_switch sw) ^ "</B>"
85 Printf.sprintf "<B>|<SUB>%d</SUB>: %s</B>" pos (render_switch sw)
86 | 1, pos when Stack.head_tag s#stack = `BranchTag ->
87 Printf.sprintf "|<SUB>%d</SUB> : %s" pos (render_switch sw)
88 | _ -> render_switch sw)
91 prerr_endline "pippo1";
93 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () markup in
94 let markup = "<metaname>" ^ markup ^ "</metaname>" in
95 prerr_endline "pippo2";
97 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw)
99 let txt0 = "<goal>" ^ sequent ^ "</goal>" in
100 "<meta number=\"" ^ (string_of_int metano) ^ "\">" ^ markup ^
101 txt0 ^ "</meta>" ^ acc
103 let res = "<metasenv>" ^
105 ~env:(render_sequent true) ~cont:(render_sequent false)
106 ~todo:(render_sequent false) "" s#stack) ^
109 prerr_endline ("sending metasenv:\n" ^ res); res
112 (* let html_of_status s =
113 let _,_,metasenv,subst,_ = s#obj in
114 let txt = List.fold_left
115 (fun acc (nmeta,_ as meta) ->
116 let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent
117 ~metasenv ~subst ~map_unicode_to_tex:false 80 s meta)
119 prerr_endline ("### txt0 = " ^ txt0);
120 ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
123 String.concat "\n\n" txt
126 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";;
129 let s = Pcre.replace ~rex:heading_nl_RE s in
131 let nl_pos = String.index s '\n' in
132 String.sub s 0 nl_pos
136 let read_file fname =
137 let chan = open_in fname in
138 let lines = ref [] in
141 lines := input_line chan :: !lines
143 with End_of_file -> close_in chan);
144 String.concat "\n" (List.rev !lines)
147 let load_index outchan =
148 let s = read_file "index.html" in
149 Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
152 let load_doc filename outchan =
153 let s = read_file filename in
155 try String.sub filename (String.length filename - 4) 4 = ".png"
156 with Invalid_argument _ -> false
158 let contenttype = if is_png then "image/png" else "text/html" in
159 Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
162 let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
163 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
164 let env = cgi#environment in
166 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
167 let sid = HExtlib.unopt sid in
170 ~content_type:"text/xml; charset=\"utf-8\""
172 let filename = cgi # argument_value "file" in
173 prerr_endline ("reading file " ^ filename);
175 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false ()
176 (read_file filename) in
177 prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND");
178 let body = "<file>" ^ body ^ "</file>" in
179 let baseuri, incpaths =
181 let root, baseuri, _fname, _tgt =
182 Librarian.baseuri_of_script ~include_paths:[] filename in
185 Str.split (Str.regexp " ")
186 (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
189 let rc = root :: includes in
190 List.iter (HLog.debug) rc; baseuri, rc
192 Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in
193 include_paths := incpaths;
194 let status = MatitaAuthentication.get_status sid in
195 MatitaAuthentication.set_status sid (status#set_baseuri baseuri);
196 cgi#out_channel#output_string body;
200 ~status:`Internal_server_error
202 ~content_type:"text/xml; charset=\"utf-8\""
204 cgi#out_channel#commit_work()
207 let advance0 sid text =
208 let status = MatitaAuthentication.get_status sid in
209 let history = MatitaAuthentication.get_history sid in
210 let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
212 eval_statement !include_paths (*buffer*) status (`Raw text)
213 (* with End_of_file -> raise Margin *)
215 MatitaAuthentication.set_status sid st;
216 MatitaAuthentication.set_history sid (st::history);
217 parsed_len, new_unparsed, st
220 let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
221 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
222 let env = cgi#environment in
225 assert (cgi#arguments <> []);
226 let uid = cgi#argument_value "userid" in
227 let userpw = cgi#argument_value "password" in
228 prerr_endline ("2: user = " ^ uid);
229 let pw,_ = MatitaAuthentication.lookup_user uid in
235 let sid = MatitaAuthentication.create_session uid in
236 let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in
237 cgi#set_header ~status:`See_other ~cache:`No_cache ~set_cookies:[cookie] ();
238 env#set_output_header_field "Location" "/index.html"
244 ~content_type:"text/html; charset=\"utf-8\""
246 cgi#out_channel#output_string
247 "<html><head></head><body>Authentication error</body></html>"
250 cgi#out_channel#commit_work()
254 (* returns the length of the executed text and an html representation of the
256 let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
257 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
258 let env = cgi#environment in
260 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
261 let sid = HExtlib.unopt sid in
264 ~content_type:"text/xml; charset=\"utf-8\""
266 let text = cgi#argument_value "body" in
267 prerr_endline ("body =\n" ^ text);
268 let parsed_len, new_unparsed, new_status = advance0 sid text in
269 let txt = output_status new_status in
271 "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
274 prerr_endline ("sending advance response:\n" ^ body);
275 cgi#out_channel#output_string body
279 ~status:`Internal_server_error
281 ~content_type:"text/xml; charset=\"utf-8\""
283 cgi#out_channel#commit_work()
286 let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
287 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
288 let env = cgi#environment in
290 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
291 let sid = HExtlib.unopt sid in
293 let rec aux parsed_len text =
295 prerr_endline ("evaluating: " ^ first_line text);
296 let plen,new_unparsed,_new_status = advance0 sid text in
297 aux (parsed_len+plen) new_unparsed
303 ~content_type:"text/xml; charset=\"utf-8\""
305 let text = cgi#argument_value "body" in
306 prerr_endline ("body =\n" ^ text);
307 let parsed_len = aux 0 text in
308 let status = MatitaAuthentication.get_status sid in
309 let txt = output_status status in
311 "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
314 prerr_endline ("sending goto bottom response:\n" ^ body);
315 cgi#out_channel#output_string body
316 with Not_found -> cgi#set_header ~status:`Internal_server_error
318 ~content_type:"text/xml; charset=\"utf-8\"" ());
319 cgi#out_channel#commit_work()
322 let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
323 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
324 let env = cgi#environment in
326 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
327 let sid = HExtlib.unopt sid in
330 ~content_type:"text/xml; charset=\"utf-8\""
332 let history = MatitaAuthentication.get_history sid in
333 let new_history,new_status =
335 _::(status::_ as history) ->
337 | [_] -> (prerr_endline "singleton";failwith "retract")
338 | _ -> (prerr_endline "nil"; assert false) in
339 NCicLibrary.time_travel new_status;
340 MatitaAuthentication.set_history sid new_history;
341 MatitaAuthentication.set_status sid new_status;
342 prerr_endline ("after retract history.length = " ^
343 string_of_int (List.length new_history));
344 let body = output_status new_status in
345 cgi#out_channel#output_string body
346 with _ -> cgi#set_header ~status:`Internal_server_error
348 ~content_type:"text/xml; charset=\"utf-8\"" ());
349 cgi#out_channel#commit_work()
353 open Netcgi1_compat.Netcgi_types;;
355 (**********************************************************************)
356 (* Create the webserver *)
357 (**********************************************************************)
361 let (opt_list, cmdline_cfg) = Netplex_main.args() in
363 let use_mt = ref true in
366 [ "-mt", Arg.Set use_mt,
367 " Use multi-threading instead of multi-processing"
372 (fun s -> raise (Arg.Bad ("Don't know what to do with: " ^ s)))
373 "usage: netplex [options]";
376 Netplex_mt.mt() (* multi-threading *)
378 Netplex_mp.mp() in (* multi-processing *)
381 { Nethttpd_services.dyn_handler = (fun _ -> process1);
382 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
383 dyn_uri = None; (* not needed *)
384 dyn_translator = (fun _ -> ""); (* not needed *)
385 dyn_accept_all_conditionals = false;
389 { Nethttpd_services.dyn_handler = (fun _ -> advance);
390 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
391 dyn_uri = None; (* not needed *)
392 dyn_translator = (fun _ -> ""); (* not needed *)
393 dyn_accept_all_conditionals = false;
396 { Nethttpd_services.dyn_handler = (fun _ -> retract);
397 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
398 dyn_uri = None; (* not needed *)
399 dyn_translator = (fun _ -> ""); (* not needed *)
400 dyn_accept_all_conditionals = false;
403 { Nethttpd_services.dyn_handler = (fun _ -> gotoBottom);
404 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
405 dyn_uri = None; (* not needed *)
406 dyn_translator = (fun _ -> ""); (* not needed *)
407 dyn_accept_all_conditionals = false;
410 { Nethttpd_services.dyn_handler = (fun _ -> retrieve);
411 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
412 dyn_uri = None; (* not needed *)
413 dyn_translator = (fun _ -> ""); (* not needed *)
414 dyn_accept_all_conditionals = false;
417 { Nethttpd_services.dyn_handler = (fun _ -> login);
418 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
419 dyn_uri = None; (* not needed *)
420 dyn_translator = (fun _ -> ""); (* not needed *)
421 dyn_accept_all_conditionals = false;
424 let nethttpd_factory =
425 Nethttpd_plex.nethttpd_factory
426 ~handlers:[ "advance", do_advance
427 ; "retract", do_retract
428 ; "bottom", goto_bottom
430 ; "login", do_login ]
432 MatitaInit.initialize_all ();
434 MatitaAuthentication.add_user "ricciott" "pippo123";
435 MatitaAuthentication.add_user "asperti" "pluto456";
439 Netplex_log.logger_factories (* allow all built-in logging styles *)
440 Netplex_workload.workload_manager_factories (* ... all ways of workload management *)
441 [ nethttpd_factory ] (* make this nethttpd available *)
445 Sys.set_signal Sys.sigpipe Sys.Signal_ignore;