4 module Stack = Continuationals.Stack
6 let rt_path () = Helm_registry.get "matita.rt_base_dir"
8 let libdir uid = (rt_path ()) ^ "/users/" ^ uid
10 let utf8_length = Netconversion.ustring_length `Enc_utf8
12 let utf8_parsed_text s floc =
13 let start, stop = HExtlib.loc_of_floc floc in
14 let len = stop - start in
15 let res = Netconversion.ustring_sub `Enc_utf8 start len s in
16 res, String.length res
18 (*** from matitaScript.ml ***)
19 (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)
21 let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script *)
24 let ast,unparsed_text =
27 (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *)
29 GrafiteParser.parsable_statement status
30 (Ulexing.from_utf8_string text) in
31 let ast = MatitaEngine.get_ast status include_paths strm in
33 | `Ast (st, text) -> st, text
35 let floc = match ast with
36 | GrafiteAst.Executable (loc, _)
37 | GrafiteAst.Comment (loc, _) -> loc in
39 let _,lend = HExtlib.loc_of_floc floc in
40 let parsed_text, _parsed_text_len =
41 utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
42 let byte_parsed_text_len = String.length parsed_text in
44 String.sub unparsed_text byte_parsed_text_len
45 (String.length unparsed_text - byte_parsed_text_len)
49 MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
51 (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*)
52 utf8_length parsed_text
54 (*let save_moo status =
55 let script = MatitaScript.current () in
56 let baseuri = status#baseuri in
57 match script#bos, script#eos with
60 GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
62 | _ -> clean_current_baseuri status
65 let sequent_size = ref 40;;
67 let include_paths = ref [];;
71 * <metaname>...</metaname>
78 let _,_,metasenv,subst,_ = s#obj in
79 let render_switch = function
80 | Stack.Open i -> "?" ^ (string_of_int i)
81 | Stack.Closed i -> "<S>?" ^ (string_of_int i) ^ "</S>"
83 let int_of_switch = function
84 | Stack.Open i | Stack.Closed i -> i
86 let sequent = function
88 let meta = List.assoc i metasenv in
89 snd (ApplyTransformation.ntxt_of_cic_sequent
90 ~metasenv ~subst ~map_unicode_to_tex:false !sequent_size s (i,meta))
91 | Stack.Closed _ -> "This goal has already been closed."
93 let render_sequent is_loc acc depth tag (pos,sw) =
94 let metano = int_of_switch sw in
97 (match depth, pos with
98 | 0, 0 -> "<B>" ^ (render_switch sw) ^ "</B>"
100 Printf.sprintf "<B>|<SUB>%d</SUB>: %s</B>" pos (render_switch sw)
101 | 1, pos when Stack.head_tag s#stack = `BranchTag ->
102 Printf.sprintf "|<SUB>%d</SUB> : %s" pos (render_switch sw)
103 | _ -> render_switch sw)
104 else render_switch sw
106 prerr_endline "pippo1";
108 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () markup in
109 let markup = "<metaname>" ^ markup ^ "</metaname>" in
110 prerr_endline "pippo2";
112 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw)
114 let txt0 = "<goal>" ^ sequent ^ "</goal>" in
115 "<meta number=\"" ^ (string_of_int metano) ^ "\">" ^ markup ^
116 txt0 ^ "</meta>" ^ acc
118 let res = "<metasenv>" ^
120 ~env:(render_sequent true) ~cont:(render_sequent false)
121 ~todo:(render_sequent false) "" s#stack) ^
124 prerr_endline ("sending metasenv:\n" ^ res); res
127 (* let html_of_status s =
128 let _,_,metasenv,subst,_ = s#obj in
129 let txt = List.fold_left
130 (fun acc (nmeta,_ as meta) ->
131 let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent
132 ~metasenv ~subst ~map_unicode_to_tex:false 80 s meta)
134 prerr_endline ("### txt0 = " ^ txt0);
135 ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
138 String.concat "\n\n" txt
141 let html_of_matita s =
142 prerr_endline ("input: " ^ s);
143 let patt1 = Str.regexp "\005" in
144 let patt2 = Str.regexp "\006" in
145 let patt3 = Str.regexp "<" in
146 let patt4 = Str.regexp ">" in
147 let res = Str.global_replace patt4 ">" s in
148 prerr_endline ("output: " ^ res);
149 let res = Str.global_replace patt3 "<" res in
150 prerr_endline ("output: " ^ res);
151 let res = Str.global_replace patt2 ">" res in
152 prerr_endline ("output: " ^ res);
153 let res = Str.global_replace patt1 "<" res in
154 prerr_endline ("output: " ^ res);
158 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";;
161 let s = Pcre.replace ~rex:heading_nl_RE s in
163 let nl_pos = String.index s '\n' in
164 String.sub s 0 nl_pos
168 let read_file fname =
169 let chan = open_in fname in
170 let lines = ref [] in
173 lines := input_line chan :: !lines
175 with End_of_file -> close_in chan);
176 String.concat "\n" (List.rev !lines)
179 let load_index outchan =
180 let s = read_file "index.html" in
181 Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
184 let load_doc filename outchan =
185 let s = read_file filename in
187 try String.sub filename (String.length filename - 4) 4 = ".png"
188 with Invalid_argument _ -> false
190 let contenttype = if is_png then "image/png" else "text/html" in
191 Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
194 let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
195 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
196 let env = cgi#environment in
198 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
199 let sid = HExtlib.unopt sid in
200 let uid = MatitaAuthentication.user_of_session sid in
203 ~content_type:"text/xml; charset=\"utf-8\""
205 let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in
206 prerr_endline ("reading file " ^ filename);
208 (* Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false ()
209 (html_of_matita (read_file filename)) in
211 html_of_matita (read_file filename) in
212 prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND");
213 let body = "<file>" ^ body ^ "</file>" in
214 let baseuri, incpaths =
216 let root, baseuri, _fname, _tgt =
217 Librarian.baseuri_of_script ~include_paths:[] filename in
220 Str.split (Str.regexp " ")
221 (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
224 let rc = root :: includes in
225 List.iter (HLog.debug) rc; baseuri, rc
227 Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in
228 include_paths := incpaths;
229 let status = MatitaAuthentication.get_status sid in
230 MatitaAuthentication.set_status sid (status#set_baseuri baseuri);
231 cgi#out_channel#output_string body;
235 ~status:`Internal_server_error
237 ~content_type:"text/xml; charset=\"utf-8\""
239 cgi#out_channel#commit_work()
242 let advance0 sid text =
243 let status = MatitaAuthentication.get_status sid in
244 let history = MatitaAuthentication.get_history sid in
245 let status = status#reset_disambiguate_db () in
246 let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
248 eval_statement !include_paths (*buffer*) status (`Raw text)
250 | HExtlib.Localized (_,e) -> raise e
251 (*| End_of_file -> raise Margin *)
253 let stringbuf = Ulexing.from_utf8_string new_statements in
254 let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in
255 let outstr = ref "" in
256 ignore (SmallLexer.mk_small_printer interpr outstr stringbuf);
257 prerr_endline ("parser output: " ^ !outstr);
258 MatitaAuthentication.set_status sid st;
259 MatitaAuthentication.set_history sid (st::history);
261 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
262 () (html_of_matita !outstr), new_unparsed, st
264 let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
265 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
266 let env = cgi#environment in
268 assert (cgi#arguments <> []);
269 let uid = cgi#argument_value "userid" in
270 let userpw = cgi#argument_value "password" in
272 MatitaAuthentication.add_user uid userpw;
273 env#set_output_header_field "Location" "/index.html"
275 | MatitaAuthentication.UsernameCollision _ ->
278 ~content_type:"text/html; charset=\"utf-8\""
280 cgi#out_channel#output_string
281 "<html><head></head><body>Error: User id collision!</body></html>"
282 | MatitaFilesystem.SvnError msg ->
285 ~content_type:"text/html; charset=\"utf-8\""
287 cgi#out_channel#output_string
288 ("<html><head></head><body><p>Error: Svn checkout failed!<p><p><textarea>"
289 ^ msg ^ "</textarea></p></body></html>"));
290 cgi#out_channel#commit_work()
293 let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
294 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
295 let env = cgi#environment in
297 assert (cgi#arguments <> []);
298 let uid = cgi#argument_value "userid" in
299 let userpw = cgi#argument_value "password" in
300 let pw,_ = MatitaAuthentication.lookup_user uid in
304 let _ = MatitaFilesystem.html_of_library uid in
305 let sid = MatitaAuthentication.create_session uid in
306 (* let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in
307 cgi#set_header ~set_cookies:[cookie] (); *)
308 env#set_output_header_field
309 "Set-Cookie" ("session=" ^ (Uuidm.to_string sid));
310 env#set_output_header_field "Location" "/index.html"
314 prerr_endline ("ERROR: received " ^ userpw ^ "but the password is " ^ pw);
317 ~content_type:"text/html; charset=\"utf-8\""
319 cgi#out_channel#output_string
320 "<html><head></head><body>Authentication error</body></html>"
323 cgi#out_channel#commit_work()
327 let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
328 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
329 let env = cgi#environment in
331 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
332 let sid = HExtlib.unopt sid in
333 MatitaAuthentication.logout_user sid;
336 ~content_type:"text/html; charset=\"utf-8\""
338 let text = read_file (rt_path () ^ "/logout.html") in
339 cgi#out_channel#output_string text
343 ~status:`Internal_server_error
345 ~content_type:"text/xml; charset=\"utf-8\""
347 cgi#out_channel#commit_work()
350 (* returns the length of the executed text and an html representation of the
352 let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
353 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
354 let env = cgi#environment in
356 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
357 let sid = HExtlib.unopt sid in
360 ~content_type:"text/xml; charset=\"utf-8\""
362 let text = cgi#argument_value "body" in
363 prerr_endline ("body =\n" ^ text);
364 let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in
365 let txt = output_status new_status in
367 "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
368 new_parsed ^ "</parsed>" ^ txt
371 prerr_endline ("sending advance response:\n" ^ body);
372 cgi#out_channel#output_string body
376 ~status:`Internal_server_error
378 ~content_type:"text/xml; charset=\"utf-8\""
380 cgi#out_channel#commit_work()
383 let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
384 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
385 let env = cgi#environment in
387 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
388 let sid = HExtlib.unopt sid in
390 let rec aux parsed_len parsed_txt text =
392 prerr_endline ("evaluating: " ^ first_line text);
393 let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in
394 aux (parsed_len+plen) (parsed_txt ^ new_parsed) new_unparsed
397 let status = MatitaAuthentication.get_status sid in
398 GrafiteTypes.Serializer.serialize
399 ~baseuri:(NUri.uri_of_string status#baseuri) status;
400 parsed_len, parsed_txt
401 | _ -> parsed_len, parsed_txt
405 ~content_type:"text/xml; charset=\"utf-8\""
407 let text = cgi#argument_value "body" in
408 prerr_endline ("body =\n" ^ text);
409 let parsed_len, new_parsed = aux 0 "" text in
410 let status = MatitaAuthentication.get_status sid in
411 let txt = output_status status in
413 "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
414 new_parsed ^ "</parsed>" ^ txt
418 "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
421 prerr_endline ("sending goto bottom response:\n" ^ body);
422 cgi#out_channel#output_string body
423 with Not_found -> cgi#set_header ~status:`Internal_server_error
425 ~content_type:"text/xml; charset=\"utf-8\"" ());
426 cgi#out_channel#commit_work()
429 let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
430 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
431 let env = cgi#environment in
433 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
434 let sid = HExtlib.unopt sid in
437 ~content_type:"text/xml; charset=\"utf-8\""
439 let history = MatitaAuthentication.get_history sid in
440 let new_history,new_status =
442 _::(status::_ as history) ->
444 | [_] -> (prerr_endline "singleton";failwith "retract")
445 | _ -> (prerr_endline "nil"; assert false) in
446 NCicLibrary.time_travel new_status;
447 MatitaAuthentication.set_history sid new_history;
448 MatitaAuthentication.set_status sid new_status;
449 prerr_endline ("after retract history.length = " ^
450 string_of_int (List.length new_history));
451 let body = output_status new_status in
452 cgi#out_channel#output_string body
453 with _ -> cgi#set_header ~status:`Internal_server_error
455 ~content_type:"text/xml; charset=\"utf-8\"" ());
456 cgi#out_channel#commit_work()
460 let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
461 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
462 let env = cgi#environment in
464 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
465 let sid = HExtlib.unopt sid in
468 ~content_type:"text/html; charset=\"utf-8\""
470 let uid = MatitaAuthentication.user_of_session sid in
472 let html = MatitaFilesystem.html_of_library uid in
473 cgi#out_channel#output_string
476 "<title>XML Tree Control</title>\n" ^
477 "<link href=\"treeview/xmlTree.css\" type=\"text/css\" rel=\"stylesheet\">\n" ^
478 "<script src=\"treeview/xmlTree.js\" type=\"text/javascript\"></script>\n" ^
480 html (* ^ "\n</body></html>" *) );
481 cgi#out_channel#commit_work()
485 let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
486 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
487 MatitaAuthentication.reset ();
490 ~content_type:"text/html; charset=\"utf-8\""
493 cgi#out_channel#output_string
495 "<title>Matitaweb Reset</title>\n" ^
496 "<body><H1>Reset completed</H1></body></html>");
497 cgi#out_channel#commit_work()
499 open Netcgi1_compat.Netcgi_types;;
501 (**********************************************************************)
502 (* Create the webserver *)
503 (**********************************************************************)
507 let (opt_list, cmdline_cfg) = Netplex_main.args() in
509 let use_mt = ref true in
512 [ "-mt", Arg.Set use_mt,
513 " Use multi-threading instead of multi-processing"
518 (fun s -> raise (Arg.Bad ("Don't know what to do with: " ^ s)))
519 "usage: netplex [options]";
522 Netplex_mt.mt() (* multi-threading *)
524 Netplex_mp.mp() in (* multi-processing *)
527 { Nethttpd_services.dyn_handler = (fun _ -> process1);
528 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
529 dyn_uri = None; (* not needed *)
530 dyn_translator = (fun _ -> ""); (* not needed *)
531 dyn_accept_all_conditionals = false;
535 { Nethttpd_services.dyn_handler = (fun _ -> advance);
536 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
537 dyn_uri = None; (* not needed *)
538 dyn_translator = (fun _ -> ""); (* not needed *)
539 dyn_accept_all_conditionals = false;
542 { Nethttpd_services.dyn_handler = (fun _ -> retract);
543 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
544 dyn_uri = None; (* not needed *)
545 dyn_translator = (fun _ -> ""); (* not needed *)
546 dyn_accept_all_conditionals = false;
549 { Nethttpd_services.dyn_handler = (fun _ -> gotoBottom);
550 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
551 dyn_uri = None; (* not needed *)
552 dyn_translator = (fun _ -> ""); (* not needed *)
553 dyn_accept_all_conditionals = false;
556 { Nethttpd_services.dyn_handler = (fun _ -> retrieve);
557 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
558 dyn_uri = None; (* not needed *)
559 dyn_translator = (fun _ -> ""); (* not needed *)
560 dyn_accept_all_conditionals = false;
563 { Nethttpd_services.dyn_handler = (fun _ -> register);
564 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
565 dyn_uri = None; (* not needed *)
566 dyn_translator = (fun _ -> ""); (* not needed *)
567 dyn_accept_all_conditionals = false;
570 { Nethttpd_services.dyn_handler = (fun _ -> login);
571 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
572 dyn_uri = None; (* not needed *)
573 dyn_translator = (fun _ -> ""); (* not needed *)
574 dyn_accept_all_conditionals = false;
577 { Nethttpd_services.dyn_handler = (fun _ -> logout);
578 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
579 dyn_uri = None; (* not needed *)
580 dyn_translator = (fun _ -> ""); (* not needed *)
581 dyn_accept_all_conditionals = false;
584 { Nethttpd_services.dyn_handler = (fun _ -> viewLib);
585 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
586 dyn_uri = None; (* not needed *)
587 dyn_translator = (fun _ -> ""); (* not needed *)
588 dyn_accept_all_conditionals = false;
591 { Nethttpd_services.dyn_handler = (fun _ -> resetLib);
592 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
593 dyn_uri = None; (* not needed *)
594 dyn_translator = (fun _ -> ""); (* not needed *)
595 dyn_accept_all_conditionals = false;
598 let nethttpd_factory =
599 Nethttpd_plex.nethttpd_factory
600 ~handlers:[ "advance", do_advance
601 ; "retract", do_retract
602 ; "bottom", goto_bottom
604 ; "register", do_register
606 ; "logout", do_logout
607 ; "reset", do_resetlib
608 ; "viewlib", do_viewlib]
610 MatitaInit.initialize_all ();
611 MatitaAuthentication.deserialize ();
614 Netplex_log.logger_factories (* allow all built-in logging styles *)
615 Netplex_workload.workload_manager_factories (* ... all ways of workload management *)
616 [ nethttpd_factory ] (* make this nethttpd available *)
620 Sys.set_signal Sys.sigpipe Sys.Signal_ignore;