| _ -> 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
~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
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\""
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
projects / helm.git / blobdiff