| _ -> 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 = "<metaname>" ^ markup ^ "</metaname>" in
- prerr_endline "pippo2";
let sequent =
Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw)
in
"<meta number=\"" ^ (string_of_int metano) ^ "\">" ^ markup ^
txt0 ^ "</meta>" ^ acc
in
- let res = "<metasenv>" ^
+ "<metasenv>" ^
(Stack.fold
~env:(render_sequent true) ~cont:(render_sequent false)
~todo:(render_sequent false) "" s#stack) ^
"</metasenv>"
- in
- prerr_endline ("sending metasenv:\n" ^ res); res
+ (* prerr_endline ("sending metasenv:\n" ^ res); res *)
;;
(* let html_of_status s =
;; *)
let html_of_matita s =
- prerr_endline ("input: " ^ 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
- prerr_endline ("output: " ^ res);
let res = Str.global_replace patt3 "<" res in
- prerr_endline ("output: " ^ res);
let res = Str.global_replace patt2 ">" res in
- prerr_endline ("output: " ^ res);
let res = Str.global_replace patt1 "<" res in
- prerr_endline ("output: " ^ res);
res
;;
();
*)
let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in
- prerr_endline ("reading file " ^ filename);
+ (* 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");
+ (* prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND"); *)
let body = "<response><file>" ^ body ^ "</file></response>" in
let baseuri, incpaths =
try
let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in
let outstr = ref "" in
ignore (SmallLexer.mk_small_printer interpr outstr stringbuf);
- prerr_endline ("parser output: " ^ !outstr);
+ (* prerr_endline ("parser output: " ^ !outstr); *)
MatitaAuthentication.set_status sid st;
parsed_len,
Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
let userpw = cgi#argument_value "password" in
(try
MatitaAuthentication.add_user uid userpw;
- env#set_output_header_field "Location" "/index.html"
+(* env#set_output_header_field "Location" "/index.html" *)
+ cgi#out_channel#output_string
+ ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/login.html\">"
+ ^ "</head><body>Redirecting to login page...</body></html>")
with
| MatitaAuthentication.UsernameCollision _ ->
cgi#set_header
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"
+(* env#set_output_header_field "Location" "/index.html" *)
+ cgi#out_channel#output_string
+ ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/index.html\">"
+ ^ "</head><body>Redirecting to Matita page...</body></html>")
end
else
begin
- prerr_endline ("ERROR: received " ^ userpw ^ "but the password is " ^ pw);
cgi#set_header
~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
let locked = cgi#argument_value "locked" in
let unlocked = cgi#argument_value "unlocked" in
let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in
- prerr_endline ("Matita will save the file for user " ^ uid);
+ let force = bool_of_string (cgi#argument_value "force") in
+
+ if ((not force) && (Sys.file_exists filename)) then
+ raise File_already_exists;
+
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...");
+ (* prerr_endline ("serializing proof objects..."); *)
GrafiteTypes.Serializer.serialize
~baseuri:(NUri.uri_of_string status#baseuri) status;
- prerr_endline ("adding to the commit queue...");
+ (* prerr_endline ("adding to the commit queue..."); *)
MatitaFilesystem.add_user uid;
- prerr_endline ("done.");
+ (* prerr_endline ("done."); *)
end;
cgi # set_header
~cache:`No_cache
();
cgi#out_channel#output_string "<response>ok</response>"
with
- | Not_found _ ->
+ | File_already_exists ->
+ cgi#out_channel#output_string "<response>cancelled</response>"
+ | Sys_error _ ->
cgi # set_header
~status:`Internal_server_error
~cache:`No_cache
();
*)
let text = cgi#argument_value "body" in
- prerr_endline ("body =\n" ^ text);
+ (* prerr_endline ("body =\n" ^ text); *)
let history = MatitaAuthentication.get_history sid in
let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in
MatitaAuthentication.set_history sid (new_status::history);
new_parsed ^ "</parsed>" ^ txt
^ "</response>"
in
- prerr_endline ("sending advance response:\n" ^ body);
+ (* prerr_endline ("sending advance response:\n" ^ body); *)
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);
+ (* prerr_endline ("body =\n" ^ text); *)
let parsed_len, new_parsed = aux 0 "" text in
let status = MatitaAuthentication.get_status sid in
let txt = output_status status in
"<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
^ "</response>"
in*)
- prerr_endline ("sending goto bottom response:\n" ^ body);
+ (* prerr_endline ("sending goto bottom response:\n" ^ body); *)
cgi # set_header
~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
+ NCicLibrary.time_travel new_status;
+ 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 "<response>ok</response>"
+ with _ ->
+ (cgi#set_header ~status:`Internal_server_error
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\"" ();
+ cgi#out_channel#output_string "<response>ok</response>");
+ 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
- prerr_endline "executing retract";
(try
let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
let sid = HExtlib.unopt sid in
history, status
| [_] -> (prerr_endline "singleton";failwith "retract")
| _ -> (prerr_endline "nil"; assert false) in
- prerr_endline "before time_travel";
NCicLibrary.time_travel new_status;
- prerr_endline "after time travel";
MatitaAuthentication.set_history sid new_history;
MatitaAuthentication.set_status sid new_status;
- prerr_endline ("after retract history.length = " ^
- string_of_int (List.length new_history));
let body = output_status new_status in
cgi # set_header
~cache:`No_cache
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;
~handlers:[ "advance", do_advance
; "retract", do_retract
; "bottom", goto_bottom
+ ; "top", goto_top
; "open", retrieve
; "register", do_register
; "login", do_login
projects / helm.git / blobdiff