- match req#path with
- | "/" -> load_index outchan
- | "/matita" -> call_service outchan
- | "/open" ->
- prerr_endline "getting 'file' argument";
- let filename = List.assoc "file" req#params_GET in
- prerr_endline ("reading file " ^ filename);
- let body =
- Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false ()
- (read_file filename) in
- prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND");
- let body = "<file>" ^ body ^ "</file>" in
- let _,baseuri,_,_ =
- Librarian.baseuri_of_script ~include_paths:[] filename
- in
- status := (!status)#set_baseuri baseuri;
- Http_daemon.respond ~code:(`Code 200) ~body outchan
- | "/advance" ->
- let script = req#body in
- prerr_endline ("body length = " ^ (string_of_int (String.length script)));
- let (parsed_len,_,txt), res, code =
- try advance script, "OK", `Code 200
- with
- | HExtlib.Localized(_,e)
- | e ->
- (prerr_endline ("exception: " ^ Printexc.to_string e);
- (try
- NTacStatus.pp_tac_status !status
- with e -> prerr_endline ("inner exception: " ^
- Printexc.to_string e));
- prerr_endline "end status";
- let txt = output_status !status in
- (0,"",txt), Printexc.to_string e, `Code 500)
- in
- (* prerr_endline ("server response:\n" ^ txt); *)
- let body =
- "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
- ^ "</response>"
- in (prerr_endline ("sending advance response:\n" ^ body);
- Http_daemon.respond ~code ~body outchan)
- | "/bottom" ->
- let script = req#body in
- prerr_endline ("body length = " ^ (string_of_int (String.length script)));
- let (parsed_len,txt), res, code =
- try gotoBottom script, "OK", `Code 200
- with
- | HExtlib.Localized(_,e)
- | e ->
- (prerr_endline ("exception: " ^ Printexc.to_string e);
- (try
- NTacStatus.pp_tac_status !status
- with e -> prerr_endline ("inner exception: " ^
- Printexc.to_string e));
- prerr_endline "end status";
- let txt = output_status !status in
- (0,txt), Printexc.to_string e, `Code 500)
- in
- (* prerr_endline ("server response:\n" ^ txt); *)
- let body =
- "<parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
- in Http_daemon.respond ~code ~body outchan
- | "/retract" ->
- (try
- let body = retract () in
- prerr_endline "retract OK";
- Http_daemon.respond ~code:(`Code 200) ~body outchan
- with e ->
- (prerr_endline (Printexc.to_string e);
- Http_daemon.respond ~code:(`Code 500) outchan))
- | url ->
- try
- let url = String.sub url 1 (String.length url - 1) in
- load_doc url outchan
- with _ -> Http_daemon.respond_not_found ~url outchan
+(* returns the length of the executed text and an html representation of the
+ * current metasenv*)
+let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+ 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);
+ let parsed_len, new_unparsed = advance0 text in
+ let txt = output_status !status in
+ let body =
+ "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
+ ^ "</response>"
+ in
+ prerr_endline ("sending advance response:\n" ^ body);
+ cgi#out_channel#output_string body;
+ cgi#out_channel#commit_work()