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 mutex = Mutex.create ();;
14 let to_be_committed = ref [];;
16 (* adds a user to the commit queue; concurrent instances possible, so we
17 * enclose the update in a CS
19 let add_user_for_commit uid =
21 to_be_committed := uid::List.filter (fun x -> x <> uid) !to_be_committed;
25 let do_global_commit () =
26 prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed);
29 let ft = MatitaAuthentication.read_ft u in
31 (* first we add new files/dirs to the repository *)
32 let to_be_added = List.map fst
33 (List.filter (fun (_,flag) -> flag = MatitaFilesystem.MAdd) ft)
37 let newout = MatitaFilesystem.add_files u to_be_added in
40 | MatitaFilesystem.SvnError outstr ->
41 prerr_endline ("ADD OF " ^ u ^ "FAILED:" ^ outstr);
45 (* now we update the local copy (to merge updates from other users) *)
47 let files,anomalies,(added,conflict,del,upd,merged) =
48 MatitaFilesystem.update_user u
50 let anomalies = String.concat "\n" anomalies in
51 let details = Printf.sprintf
53 "%d deleted files\n"^^
54 "%d updated files\n"^^
56 "%d conflicting files\n\n" ^^
57 "Anomalies:\n%s") added del upd merged conflict anomalies
59 prerr_endline ("update details:\n" ^ details);
60 MatitaAuthentication.set_file_flag u files;
63 | MatitaFilesystem.SvnError outstr ->
64 prerr_endline ("UPDATE OF " ^ u ^ "FAILED:" ^ outstr);
68 (* we re-read the file table after updating *)
69 let ft = MatitaAuthentication.read_ft u in
71 (* finally we perform the real commit *)
72 let modified = (List.map fst
73 (List.filter (fun (_,flag) -> flag = MatitaFilesystem.MModified) ft))
75 let to_be_committed = to_be_added @ modified
78 let newout = MatitaFilesystem.commit u to_be_committed in
81 | MatitaFilesystem.SvnError outstr ->
82 prerr_endline ("COMMIT OF " ^ u ^ "FAILED:" ^ outstr);
86 (* call stat to get the final status *)
87 let files, anomalies = MatitaFilesystem.stat_user u in
88 let added,not_added = List.fold_left
89 (fun (a_acc, na_acc) fname ->
90 if List.mem fname (List.map fst files) then
96 let committed,not_committed = List.fold_left
97 (fun (c_acc, nc_acc) fname ->
98 if List.mem fname (List.map fst files) then
101 fname::c_acc, nc_acc)
104 let conflicts = List.map fst (List.filter
105 (fun (_,f) -> f = Some MatitaFilesystem.MConflict) files)
107 MatitaAuthentication.set_file_flag u
108 (List.map (fun x -> x, Some MatitaFilesystem.MSynchronized) (added@committed));
109 MatitaAuthentication.set_file_flag u files;
110 out ^ "\n\n" ^ (Printf.sprintf
111 ("COMMIT RESULTS for %s\n" ^^
112 "==============\n" ^^
113 "added and committed (%d of %d): %s\n" ^^
114 "modified and committed (%d of %d): %s\n" ^^
116 "not committed: %s\n" ^^
118 u (List.length added) (List.length to_be_added) (String.concat ", " added)
119 (List.length committed) (List.length modified) (String.concat ", " committed)
120 (String.concat ", " not_added)
121 (String.concat ", " not_committed) (String.concat ", " conflicts)))
123 "" (List.rev !to_be_committed)
126 (*** from matitaScript.ml ***)
127 (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)
129 let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script *)
132 let ast,unparsed_text =
135 (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *)
137 GrafiteParser.parsable_statement status
138 (Ulexing.from_utf8_string text) in
139 let ast = MatitaEngine.get_ast status include_paths strm in
141 | `Ast (st, text) -> st, text
143 let floc = match ast with
144 | GrafiteAst.Executable (loc, _)
145 | GrafiteAst.Comment (loc, _) -> loc in
147 let _,lend = HExtlib.loc_of_floc floc in
148 let parsed_text, _parsed_text_len =
149 HExtlib.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
150 let byte_parsed_text_len = String.length parsed_text in
152 String.sub unparsed_text byte_parsed_text_len
153 (String.length unparsed_text - byte_parsed_text_len)
157 MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
159 (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*)
160 utf8_length parsed_text
162 (*let save_moo status =
163 let script = MatitaScript.current () in
164 let baseuri = status#baseuri in
165 match script#bos, script#eos with
168 GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
170 | _ -> clean_current_baseuri status
173 let sequent_size = ref 40;;
175 let include_paths = ref [];;
178 * <meta number="...">
179 * <metaname>...</metaname>
185 let output_status s =
186 let _,_,metasenv,subst,_ = s#obj in
187 let render_switch = function
188 | Stack.Open i -> "?" ^ (string_of_int i)
189 | Stack.Closed i -> "<S>?" ^ (string_of_int i) ^ "</S>"
191 let int_of_switch = function
192 | Stack.Open i | Stack.Closed i -> i
194 let sequent = function
196 let meta = List.assoc i metasenv in
197 snd (ApplyTransformation.ntxt_of_cic_sequent
198 ~metasenv ~subst ~map_unicode_to_tex:false !sequent_size s (i,meta))
199 | Stack.Closed _ -> "This goal has already been closed."
201 let render_sequent is_loc acc depth tag (pos,sw) =
202 let metano = int_of_switch sw in
205 (match depth, pos with
206 | 0, 0 -> "<span class=\"activegoal\">" ^ (render_switch sw) ^ "</span>"
208 Printf.sprintf "<span class=\"activegoal\">|<SUB>%d</SUB>: %s</span>" pos (render_switch sw)
209 | 1, pos when Stack.head_tag s#stack = `BranchTag ->
210 Printf.sprintf "<span class=\"passivegoal\">|<SUB>%d</SUB> : %s</span>" pos (render_switch sw)
211 | _ -> render_switch sw)
212 else render_switch sw
215 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () markup in
216 let markup = "<metaname>" ^ markup ^ "</metaname>" in
218 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw)
220 let txt0 = "<goal>" ^ sequent ^ "</goal>" in
221 "<meta number=\"" ^ (string_of_int metano) ^ "\">" ^ markup ^
222 txt0 ^ "</meta>" ^ acc
226 ~env:(render_sequent true) ~cont:(render_sequent false)
227 ~todo:(render_sequent false) "" s#stack) ^
229 (* prerr_endline ("sending metasenv:\n" ^ res); res *)
232 let html_of_matita s =
233 let patt1 = Str.regexp "\005" in
234 let patt2 = Str.regexp "\006" in
235 let patt3 = Str.regexp "<" in
236 let patt4 = Str.regexp ">" in
237 let res = Str.global_replace patt4 ">" s in
238 let res = Str.global_replace patt3 "<" res in
239 let res = Str.global_replace patt2 ">" res in
240 let res = Str.global_replace patt1 "<" res in
244 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";;
247 let s = Pcre.replace ~rex:heading_nl_RE s in
249 let nl_pos = String.index s '\n' in
250 String.sub s 0 nl_pos
254 let read_file fname =
255 let chan = open_in fname in
256 let lines = ref [] in
259 lines := input_line chan :: !lines
261 with End_of_file -> close_in chan);
262 String.concat "\n" (List.rev !lines)
265 let load_index outchan =
266 let s = read_file "index.html" in
267 Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
270 let load_doc filename outchan =
271 let s = read_file filename in
273 try String.sub filename (String.length filename - 4) 4 = ".png"
274 with Invalid_argument _ -> false
276 let contenttype = if is_png then "image/png" else "text/html" in
277 Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
280 let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
281 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
282 let env = cgi#environment in
284 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
285 let sid = HExtlib.unopt sid in
286 let uid = MatitaAuthentication.user_of_session sid in
290 ~content_type:"text/xml; charset=\"utf-8\""
293 let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in
294 (* prerr_endline ("reading file " ^ filename); *)
296 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false ()
297 (html_of_matita (read_file filename)) in
299 (* html_of_matita (read_file filename) in *)
300 (* prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND"); *)
301 let body = "<response><file>" ^ body ^ "</file></response>" in
302 let baseuri, incpaths =
304 let root, baseuri, _fname, _tgt =
305 Librarian.baseuri_of_script ~include_paths:[] filename in
308 Str.split (Str.regexp " ")
309 (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
312 let rc = root :: includes in
313 List.iter (HLog.debug) rc; baseuri, rc
315 Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in
316 include_paths := incpaths;
317 let status = (MatitaAuthentication.get_status sid)#set_baseuri baseuri in
318 let history = [status] in
319 MatitaAuthentication.set_status sid status;
320 MatitaAuthentication.set_history sid history;
323 ~content_type:"text/xml; charset=\"utf-8\""
325 cgi#out_channel#output_string body;
329 ~status:`Internal_server_error
331 ~content_type:"text/html; charset=\"utf-8\""
333 cgi#out_channel#commit_work()
336 let advance0 sid text =
337 let status = MatitaAuthentication.get_status sid in
338 let status = status#reset_disambiguate_db () in
339 let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
341 eval_statement !include_paths (*buffer*) status (`Raw text)
343 | HExtlib.Localized (_,e) -> raise e
344 (*| End_of_file -> raise Margin *)
346 let stringbuf = Ulexing.from_utf8_string new_statements in
347 let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in
348 let outstr = ref "" in
349 ignore (SmallLexer.mk_small_printer interpr outstr stringbuf);
350 prerr_endline ("baseuri after advance = " ^ st#baseuri);
351 (* prerr_endline ("parser output: " ^ !outstr); *)
352 MatitaAuthentication.set_status sid st;
354 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
355 () (html_of_matita !outstr), new_unparsed, st
357 let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
358 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
359 let _env = cgi#environment in
361 assert (cgi#arguments <> []);
362 let uid = cgi#argument_value "userid" in
363 let userpw = cgi#argument_value "password" in
365 MatitaAuthentication.add_user uid userpw;
366 (* env#set_output_header_field "Location" "/index.html" *)
367 cgi#out_channel#output_string
368 ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/login.html\">"
369 ^ "</head><body>Redirecting to login page...</body></html>")
371 | MatitaAuthentication.UsernameCollision _ ->
374 ~content_type:"text/html; charset=\"utf-8\""
376 cgi#out_channel#output_string
377 "<html><head></head><body>Error: User id collision!</body></html>"
378 | MatitaFilesystem.SvnError msg ->
381 ~content_type:"text/html; charset=\"utf-8\""
383 cgi#out_channel#output_string
384 ("<html><head></head><body><p>Error: Svn checkout failed!<p><p><textarea>"
385 ^ msg ^ "</textarea></p></body></html>"));
386 cgi#out_channel#commit_work()
389 let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
390 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
391 let env = cgi#environment in
393 assert (cgi#arguments <> []);
394 let uid = cgi#argument_value "userid" in
395 let userpw = cgi#argument_value "password" in
396 let pw,_ = MatitaAuthentication.lookup_user uid in
400 let ft = MatitaAuthentication.read_ft uid in
401 let _ = MatitaFilesystem.html_of_library uid ft in
402 let sid = MatitaAuthentication.create_session uid in
403 (* let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in
404 cgi#set_header ~set_cookies:[cookie] (); *)
405 env#set_output_header_field
406 "Set-Cookie" ("session=" ^ (Uuidm.to_string sid));
407 (* env#set_output_header_field "Location" "/index.html" *)
408 cgi#out_channel#output_string
409 ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/index.html\">"
410 ^ "</head><body>Redirecting to Matita page...</body></html>")
416 ~content_type:"text/html; charset=\"utf-8\""
418 cgi#out_channel#output_string
419 "<html><head></head><body>Authentication error</body></html>"
422 cgi#out_channel#commit_work()
426 let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
427 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
428 let env = cgi#environment in
430 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
431 let sid = HExtlib.unopt sid in
432 MatitaAuthentication.logout_user sid;
435 ~content_type:"text/html; charset=\"utf-8\""
437 let text = read_file (rt_path () ^ "/logout.html") in
438 cgi#out_channel#output_string text
442 ~status:`Internal_server_error
444 ~content_type:"text/html; charset=\"utf-8\""
446 cgi#out_channel#commit_work()
449 exception File_already_exists;;
451 let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
452 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
453 let env = cgi#environment in
455 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
456 let sid = HExtlib.unopt sid in
457 let status = MatitaAuthentication.get_status sid in
458 let uid = MatitaAuthentication.user_of_session sid in
459 assert (cgi#arguments <> []);
460 let locked = cgi#argument_value "locked" in
461 let unlocked = cgi#argument_value "unlocked" in
462 let dir = cgi#argument_value "dir" in
463 let rel_filename = cgi # argument_value "file" in
464 let filename = libdir uid ^ "/" ^ rel_filename in
465 let force = bool_of_string (cgi#argument_value "force") in
466 let already_exists = Sys.file_exists filename in
468 if ((not force) && already_exists) then
469 raise File_already_exists;
472 Unix.mkdir filename 0o744
475 let oc = open_out filename in
476 output_string oc (locked ^ unlocked);
478 if MatitaEngine.eos status unlocked then
480 (* prerr_endline ("serializing proof objects..."); *)
481 GrafiteTypes.Serializer.serialize
482 ~baseuri:(NUri.uri_of_string status#baseuri) status;
483 (* prerr_endline ("adding to the commit queue..."); *)
484 add_user_for_commit uid;
485 (* prerr_endline ("done."); *)
490 List.assoc rel_filename (MatitaAuthentication.read_ft uid)
491 with Not_found -> MatitaFilesystem.MUnversioned
493 (if old_flag <> MatitaFilesystem.MConflict &&
494 old_flag <> MatitaFilesystem.MAdd then
496 if already_exists then MatitaFilesystem.MModified
497 else MatitaFilesystem.MAdd
499 MatitaAuthentication.set_file_flag uid [rel_filename, Some newflag]);
502 ~content_type:"text/xml; charset=\"utf-8\""
504 cgi#out_channel#output_string "<response>ok</response>"
506 | File_already_exists ->
507 cgi#out_channel#output_string "<response>cancelled</response>"
510 ~status:`Internal_server_error
512 ~content_type:"text/xml; charset=\"utf-8\""
515 let estr = Printexc.to_string e in
516 cgi#out_channel#output_string ("<response>" ^ estr ^ "</response>"));
517 cgi#out_channel#commit_work()
520 let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
521 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
522 let _env = cgi#environment in
524 let out = do_global_commit () in
527 ~content_type:"text/xml; charset=\"utf-8\""
529 cgi#out_channel#output_string "<commit>";
530 cgi#out_channel#output_string "<response>ok</response>";
531 cgi#out_channel#output_string ("<details>" ^ out ^ "</details>");
532 cgi#out_channel#output_string "</commit>"
536 ~status:`Internal_server_error
538 ~content_type:"text/xml; charset=\"utf-8\""
540 cgi#out_channel#commit_work()
543 let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
544 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
545 let env = cgi#environment in
546 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
547 let sid = HExtlib.unopt sid in
548 let uid = MatitaAuthentication.user_of_session sid in
550 let files,anomalies,(added,conflict,del,upd,merged) =
551 MatitaFilesystem.update_user uid
553 let anomalies = String.concat "\n" anomalies in
554 let details = Printf.sprintf
556 "%d deleted files\n"^^
557 "%d updated files\n"^^
558 "%d merged files\n"^^
559 "%d conflicting files\n\n" ^^
560 "Anomalies:\n%s") added del upd merged conflict anomalies
562 prerr_endline ("update details:\n" ^ details);
564 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () details
566 MatitaAuthentication.set_file_flag uid files;
569 ~content_type:"text/xml; charset=\"utf-8\""
571 cgi#out_channel#output_string "<update>";
572 cgi#out_channel#output_string "<response>ok</response>";
573 cgi#out_channel#output_string ("<details>" ^ details ^ "</details>");
574 cgi#out_channel#output_string "</update>";
578 ~status:`Internal_server_error
580 ~content_type:"text/xml; charset=\"utf-8\""
582 cgi#out_channel#commit_work()
585 (* returns the length of the executed text and an html representation of the
587 let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
588 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
589 let env = cgi#environment in
591 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
592 let sid = HExtlib.unopt sid in
596 ~content_type:"text/xml; charset=\"utf-8\""
599 let text = cgi#argument_value "body" in
600 (* prerr_endline ("body =\n" ^ text); *)
601 let history = MatitaAuthentication.get_history sid in
602 let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in
603 MatitaAuthentication.set_history sid (new_status::history);
604 let txt = output_status new_status in
606 "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
607 new_parsed ^ "</parsed>" ^ txt
610 (* prerr_endline ("sending advance response:\n" ^ body); *)
613 ~content_type:"text/xml; charset=\"utf-8\""
615 cgi#out_channel#output_string body
619 ~status:`Internal_server_error
621 ~content_type:"text/xml; charset=\"utf-8\""
623 cgi#out_channel#commit_work()
626 let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
627 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
628 let env = cgi#environment in
630 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
631 let sid = HExtlib.unopt sid in
632 let history = MatitaAuthentication.get_history sid in
634 let rec aux parsed_len parsed_txt text =
636 prerr_endline ("evaluating: " ^ first_line text);
637 let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in
638 aux (parsed_len+plen) (parsed_txt ^ new_parsed) new_unparsed
641 let status = MatitaAuthentication.get_status sid in
642 GrafiteTypes.Serializer.serialize
643 ~baseuri:(NUri.uri_of_string status#baseuri) status;
644 if parsed_len > 0 then
645 MatitaAuthentication.set_history sid (status::history);
646 parsed_len, parsed_txt
647 | _ -> parsed_len, parsed_txt
652 ~content_type:"text/xml; charset=\"utf-8\""
655 let text = cgi#argument_value "body" in
656 (* prerr_endline ("body =\n" ^ text); *)
657 let parsed_len, new_parsed = aux 0 "" text in
658 let status = MatitaAuthentication.get_status sid in
659 let txt = output_status status in
661 "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
662 new_parsed ^ "</parsed>" ^ txt
666 "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
669 (* prerr_endline ("sending goto bottom response:\n" ^ body); *)
672 ~content_type:"text/xml; charset=\"utf-8\""
674 cgi#out_channel#output_string body
675 with Not_found -> cgi#set_header ~status:`Internal_server_error
677 ~content_type:"text/xml; charset=\"utf-8\"" ());
678 cgi#out_channel#commit_work()
681 let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
682 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
683 let env = cgi#environment in
684 prerr_endline "executing goto Top";
686 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
687 let sid = HExtlib.unopt sid in
691 ~content_type:"text/xml; charset=\"utf-8\""
694 let status = MatitaAuthentication.get_status sid in
695 let uid = MatitaAuthentication.user_of_session sid in
696 let baseuri = status#baseuri in
697 let new_status = new MatitaEngine.status (Some uid) baseuri in
698 prerr_endline "gototop prima della time travel";
699 NCicLibrary.time_travel new_status;
700 prerr_endline "gototop dopo della time travel";
701 let new_history = [new_status] in
702 MatitaAuthentication.set_history sid new_history;
703 MatitaAuthentication.set_status sid new_status;
704 NCicLibrary.time_travel new_status;
707 ~content_type:"text/xml; charset=\"utf-8\""
709 cgi#out_channel#output_string "<response>ok</response>"
711 (cgi#set_header ~status:`Internal_server_error
713 ~content_type:"text/xml; charset=\"utf-8\"" ();
714 cgi#out_channel#output_string "<response>ok</response>"));
715 cgi#out_channel#commit_work()
718 let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
719 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
720 let env = cgi#environment in
722 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
723 let sid = HExtlib.unopt sid in
727 ~content_type:"text/xml; charset=\"utf-8\""
730 let history = MatitaAuthentication.get_history sid in
731 let new_history,new_status =
733 _::(status::_ as history) ->
735 | [_] -> (prerr_endline "singleton";failwith "retract")
736 | _ -> (prerr_endline "nil"; assert false) in
737 prerr_endline ("prima della time travel");
738 NCicLibrary.time_travel new_status;
739 prerr_endline ("dopo della time travel");
740 MatitaAuthentication.set_history sid new_history;
741 MatitaAuthentication.set_status sid new_status;
742 prerr_endline ("baseuri after retract = " ^ new_status#baseuri);
743 let body = output_status new_status in
746 ~content_type:"text/xml; charset=\"utf-8\""
748 cgi#out_channel#output_string body
749 with _ -> cgi#set_header ~status:`Internal_server_error
751 ~content_type:"text/xml; charset=\"utf-8\"" ());
752 cgi#out_channel#commit_work()
756 let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
757 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
758 let env = cgi#environment in
760 let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
761 let sid = HExtlib.unopt sid in
765 ~content_type:"text/html; charset=\"utf-8\""
768 let uid = MatitaAuthentication.user_of_session sid in
770 let ft = MatitaAuthentication.read_ft uid in
771 let html = MatitaFilesystem.html_of_library uid ft in
774 ~content_type:"text/html; charset=\"utf-8\""
776 cgi#out_channel#output_string
779 "<title>XML Tree Control</title>\n" ^
780 "<link href=\"treeview/xmlTree.css\" type=\"text/css\" rel=\"stylesheet\">\n" ^
781 "<script src=\"treeview/xmlTree.js\" type=\"text/javascript\"></script>\n" ^
783 html (* ^ "\n</body></html>" *) );
785 let files,anomalies = MatitaFilesystem.stat_user uid in
786 let changed = HExtlib.filter_map
787 (fun (n,f) -> if (f = Some MatitaFilesystem.MModified) then Some n else None) files
789 let changed = String.concat "\n" changed in
790 let anomalies = String.concat "\n" anomalies in
791 prerr_endline ("Changed:\n" ^ changed ^ "\n\nAnomalies:\n" ^ anomalies);
792 cgi#out_channel#commit_work()
796 let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
797 let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
798 MatitaAuthentication.reset ();
801 ~content_type:"text/html; charset=\"utf-8\""
804 cgi#out_channel#output_string
806 "<title>Matitaweb Reset</title>\n" ^
807 "<body><H1>Reset completed</H1></body></html>");
808 cgi#out_channel#commit_work()
810 open Netcgi1_compat.Netcgi_types;;
812 (**********************************************************************)
813 (* Create the webserver *)
814 (**********************************************************************)
818 let (opt_list, cmdline_cfg) = Netplex_main.args() in
820 let use_mt = ref true in
823 [ "-mt", Arg.Set use_mt,
824 " Use multi-threading instead of multi-processing"
829 (fun s -> raise (Arg.Bad ("Don't know what to do with: " ^ s)))
830 "usage: netplex [options]";
833 Netplex_mt.mt() (* multi-threading *)
835 Netplex_mp.mp() in (* multi-processing *)
838 { Nethttpd_services.dyn_handler = (fun _ -> process1);
839 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
840 dyn_uri = None; (* not needed *)
841 dyn_translator = (fun _ -> ""); (* not needed *)
842 dyn_accept_all_conditionals = false;
846 { Nethttpd_services.dyn_handler = (fun _ -> advance);
847 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
848 dyn_uri = None; (* not needed *)
849 dyn_translator = (fun _ -> ""); (* not needed *)
850 dyn_accept_all_conditionals = false;
853 { Nethttpd_services.dyn_handler = (fun _ -> retract);
854 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
855 dyn_uri = None; (* not needed *)
856 dyn_translator = (fun _ -> ""); (* not needed *)
857 dyn_accept_all_conditionals = false;
860 { Nethttpd_services.dyn_handler = (fun _ -> gotoBottom);
861 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
862 dyn_uri = None; (* not needed *)
863 dyn_translator = (fun _ -> ""); (* not needed *)
864 dyn_accept_all_conditionals = false;
867 { Nethttpd_services.dyn_handler = (fun _ -> gotoTop);
868 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
869 dyn_uri = None; (* not needed *)
870 dyn_translator = (fun _ -> ""); (* not needed *)
871 dyn_accept_all_conditionals = false;
874 { Nethttpd_services.dyn_handler = (fun _ -> retrieve);
875 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
876 dyn_uri = None; (* not needed *)
877 dyn_translator = (fun _ -> ""); (* not needed *)
878 dyn_accept_all_conditionals = false;
881 { Nethttpd_services.dyn_handler = (fun _ -> register);
882 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
883 dyn_uri = None; (* not needed *)
884 dyn_translator = (fun _ -> ""); (* not needed *)
885 dyn_accept_all_conditionals = false;
888 { Nethttpd_services.dyn_handler = (fun _ -> login);
889 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
890 dyn_uri = None; (* not needed *)
891 dyn_translator = (fun _ -> ""); (* not needed *)
892 dyn_accept_all_conditionals = false;
895 { Nethttpd_services.dyn_handler = (fun _ -> logout);
896 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
897 dyn_uri = None; (* not needed *)
898 dyn_translator = (fun _ -> ""); (* not needed *)
899 dyn_accept_all_conditionals = false;
902 { Nethttpd_services.dyn_handler = (fun _ -> viewLib);
903 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
904 dyn_uri = None; (* not needed *)
905 dyn_translator = (fun _ -> ""); (* not needed *)
906 dyn_accept_all_conditionals = false;
909 { Nethttpd_services.dyn_handler = (fun _ -> resetLib);
910 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
911 dyn_uri = None; (* not needed *)
912 dyn_translator = (fun _ -> ""); (* not needed *)
913 dyn_accept_all_conditionals = false;
916 { Nethttpd_services.dyn_handler = (fun _ -> save);
917 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
918 dyn_uri = None; (* not needed *)
919 dyn_translator = (fun _ -> ""); (* not needed *)
920 dyn_accept_all_conditionals = false;
923 { Nethttpd_services.dyn_handler = (fun _ -> initiate_commit);
924 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
925 dyn_uri = None; (* not needed *)
926 dyn_translator = (fun _ -> ""); (* not needed *)
927 dyn_accept_all_conditionals = false;
930 { Nethttpd_services.dyn_handler = (fun _ -> svn_update);
931 dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
932 dyn_uri = None; (* not needed *)
933 dyn_translator = (fun _ -> ""); (* not needed *)
934 dyn_accept_all_conditionals = false;
938 let nethttpd_factory =
939 Nethttpd_plex.nethttpd_factory
940 ~handlers:[ "advance", do_advance
941 ; "retract", do_retract
942 ; "bottom", goto_bottom
945 ; "register", do_register
947 ; "logout", do_logout
948 ; "reset", do_resetlib
949 ; "viewlib", do_viewlib
951 ; "commit", do_commit
952 ; "update", do_update]
954 MatitaInit.initialize_all ();
955 MatitaAuthentication.deserialize ();
958 Netplex_log.logger_factories (* allow all built-in logging styles *)
959 Netplex_workload.workload_manager_factories (* ... all ways of workload management *)
960 [ nethttpd_factory ] (* make this nethttpd available *)
964 Sys.set_signal Sys.sigpipe Sys.Signal_ignore;