+ let strchoices =
+ String.concat "\n"
+ (List.map (fun x -> tag_of_choice (choice_of_alias x)) choices)
+ in
+ prerr_endline (Printf.sprintf
+ "@@@ Ambiguous input at (%d,%d). Possible choices:\n\n%s\n\n@@@ End."
+ x y strchoices);
+ (*
+ let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in
+ let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in
+ let post = Netconversion.ustring_sub `Enc_utf8 y
+ (Netconversion.ustring_length `Enc_utf8 text - y) text in
+ let title = "Disambiguation Error" in
+ (* let title = "" in *)
+ let marked =
+ pre ^ "\005span class=\"error\" title=\"" ^ title ^ "\"\006" ^ err ^ "\005/span\006" ^ post in
+ let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
+ () (html_of_matita marked) in
+ *)
+ let strchoices = Printf.sprintf
+ "<ambiguity start=\"%d\" stop=\"%d\">%s</ambiguity>" x y strchoices
+ in raise (Disamb_error strchoices)
+ | GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l))
+ (* | End_of_file -> ... *)
+ | e ->
+ (* prerr_endline ("matitadaemon *** Unhandled exception " ^ Printexc.to_string e); *)
+ prerr_endline ("matitadaemon *** Unhandled exception " ^ snd (MatitaExcPp.to_string e));
+ raise e
+ in
+
+ try
+ eval_statement !include_paths (*buffer*) status (`Raw text)
+ with e -> do_exc e
+ in
+ debug "BEGIN PRINTGRAMMAR";
+ (*prerr_endline (Print_grammar.ebnf_of_term status);*)
+ (*let kwds = String.concat ", " status#get_kwds in
+ debug ("keywords = " ^ kwds );*)
+ debug "END PRINTGRAMMAR";
+ MatitaAuthentication.set_status sid st;
+ MatitaAuthentication.set_history sid (st::history);
+(* prerr_endline "previous timestamp";
+ status#print_timestamp();
+ prerr_endline "current timestamp";
+ st#print_timestamp(); *)
+ parsed_len,
+ Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
+ () (html_of_matita new_statements), new_unparsed, st
+
+let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+ let _env = cgi#environment in
+
+ assert (cgi#arguments <> []);
+ let uid = cgi#argument_value "userid" in
+ let userpw = cgi#argument_value "password" in
+ (try
+ (* currently registering only unprivileged users *)
+ MatitaAuthentication.add_user uid userpw false;
+(* 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
+ ~cache:`No_cache
+ ~content_type:"text/html; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string
+ "<html><head></head><body>Error: User id collision!</body></html>"
+ | MatitaFilesystem.SvnError msg ->
+ cgi#set_header
+ ~cache:`No_cache
+ ~content_type:"text/html; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string
+ ("<html><head></head><body><p>Error: Svn checkout failed!<p><p><textarea>"
+ ^ msg ^ "</textarea></p></body></html>"));
+ cgi#out_channel#commit_work()
+;;
+
+let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+ let env = cgi#environment in
+
+ assert (cgi#arguments <> []);
+ let uid = cgi#argument_value "userid" in
+ let userpw = cgi#argument_value "password" in
+ (try
+ MatitaAuthentication.check_pw uid userpw;
+ NCicLibrary.init (Some uid);
+ let ft = MatitaAuthentication.read_ft uid in
+ let _ = MatitaFilesystem.html_of_library uid ft in
+ let sid = MatitaAuthentication.create_session uid in
+ (* let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in
+ 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" *)
+ cgi#out_channel#output_string
+ ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/index.html\">"
+ ^ "</head><body>Redirecting to Matita page...</body></html>")
+ with MatitaAuthentication.InvalidPassword ->
+ cgi#set_header
+ ~cache:`No_cache
+ ~content_type:"text/html; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string
+ "<html><head></head><body>Authentication error</body></html>");
+ cgi#out_channel#commit_work()
+;;
+
+let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+ let env = cgi#environment in
+ (try
+ let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+ let sid = HExtlib.unopt sid in
+ MatitaAuthentication.logout_user sid;
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/html; charset=\"utf-8\""
+ ();
+ let text = read_file (rt_path () ^ "/logout.html") in
+ cgi#out_channel#output_string text
+ with
+ | Not_found _ ->
+ cgi # set_header
+ ~status:`Internal_server_error
+ ~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
+ (try
+ let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+ let sid = HExtlib.unopt sid in
+ let status = MatitaAuthentication.get_status sid in
+ let uid = MatitaAuthentication.user_of_session sid in
+ assert (cgi#arguments <> []);
+ let locked = cgi#argument_value "locked" in
+ let unlocked = cgi#argument_value "unlocked" in
+ let dir = cgi#argument_value "dir" in
+ let rel_filename = cgi # argument_value "file" in
+ let filename = libdir uid ^ "/" ^ rel_filename in
+ let force = bool_of_string (cgi#argument_value "force") in
+ let already_exists = Sys.file_exists filename in
+
+ if ((not force) && already_exists) then
+ raise File_already_exists;
+
+ if dir = "true" then
+ Unix.mkdir filename 0o744
+ else
+ begin
+ 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..."); *)
+ GrafiteTypes.Serializer.serialize
+ ~baseuri:(NUri.uri_of_string status#baseuri) status;
+ (* prerr_endline ("done."); *)
+ end;
+ end;
+ let old_flag =
+ try
+ List.assoc rel_filename (MatitaAuthentication.read_ft uid)
+ with Not_found -> MatitaFilesystem.MUnversioned
+ in
+ (if old_flag <> MatitaFilesystem.MConflict &&
+ old_flag <> MatitaFilesystem.MAdd then
+ let newflag =
+ if already_exists then MatitaFilesystem.MModified
+ else MatitaFilesystem.MAdd
+ in
+ MatitaAuthentication.set_file_flag uid [rel_filename, Some newflag]);
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string "<response>ok</response>"
+ with
+ | File_already_exists ->
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string "<response>cancelled</response>"
+ | Sys_error _ ->
+ cgi # set_header
+ ~status:`Internal_server_error
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ()
+ | e ->
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ let estr = Printexc.to_string e in
+ cgi#out_channel#output_string ("<response>" ^ estr ^ "</response>"));
+ cgi#out_channel#commit_work()
+;;
+
+let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+ let env = cgi#environment in
+ (try
+ let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+ let sid = HExtlib.unopt sid in
+ MatitaAuthentication.probe_commit_priv sid;
+ let uid = MatitaAuthentication.user_of_session sid in
+ let out = do_global_commit (* () *) uid in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string "<commit>";
+ cgi#out_channel#output_string "<response>ok</response>";
+ cgi#out_channel#output_string ("<details>" ^ out ^ "</details>");
+ cgi#out_channel#output_string "</commit>"
+ with
+ | Failure _ ->
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string
+ "<commit><error>no commit privileges</error></commit>"
+ | Not_found _ ->
+ cgi # set_header
+ ~status:`Internal_server_error
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ());
+ cgi#out_channel#commit_work()
+;;
+
+let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+ let env = cgi#environment in
+ let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+ let sid = HExtlib.unopt sid in
+ let uid = MatitaAuthentication.user_of_session sid in
+ (try
+ MatitaAuthentication.probe_commit_priv sid;
+ let files,anomalies,(added,conflict,del,upd,merged) =
+ MatitaFilesystem.update_user uid
+ in
+ let anomalies = String.concat "\n" anomalies in
+ let details = Printf.sprintf
+ ("%d new files\n"^^
+ "%d deleted files\n"^^
+ "%d updated files\n"^^
+ "%d merged files\n"^^
+ "%d conflicting files\n\n" ^^
+ "Anomalies:\n%s") added del upd merged conflict anomalies
+ in
+ prerr_endline ("update details:\n" ^ details);
+ let details =
+ Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () details
+ in
+ MatitaAuthentication.set_file_flag uid files;
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string "<update>";
+ cgi#out_channel#output_string "<response>ok</response>";
+ cgi#out_channel#output_string ("<details>" ^ details ^ "</details>");
+ cgi#out_channel#output_string "</update>";
+ with
+ | Failure _ ->
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string
+ "<commit><error>no commit privileges</error></commit>"
+ | Not_found _ ->
+ cgi # set_header
+ ~status:`Internal_server_error
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ());
+ cgi#out_channel#commit_work()
+;;
+
+(* returns the length of the executed text and an html representation of the
+ * current metasenv*)
+(*let advance =*)
+let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+ let env = cgi#environment in
+ (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 text = cgi#argument_value "body" in
+ (* prerr_endline ("body =\n" ^ text); *)
+ let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in
+ let txt = output_status new_status in
+ let body =
+ "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
+ new_parsed ^ "</parsed>" ^ txt
+ ^ "</response>"
+ in
+ (* prerr_endline ("sending advance response:\n" ^ body); *)
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string body
+ with
+ | Generic_error text ->
+ let body = "<response><error>" ^ text ^ "</error></response>" in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string body
+ | Emphasized_error text ->
+(* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> *)
+ let body = "<response><localized>" ^ text ^ "</localized></response>" in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string body
+ | Disamb_error text ->
+ let body = "<response>" ^ text ^ "</response>" in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string body
+ | End_of_file _ ->
+ let body = "<response><parsed length=\"0\"></parsed></response>" in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string body
+ | Not_found _ ->
+ cgi # set_header
+ ~status:`Internal_server_error
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ()
+ );
+ cgi#out_channel#commit_work()
+;;
+
+let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+ let env = cgi#environment in
+(* (try *)
+ let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+ let sid = HExtlib.unopt sid in
+
+ let error_msg = function
+ | Emphasized_error text -> "<localized>" ^ text ^ "</localized>"
+ | Disamb_error text -> text
+ | End_of_file _ -> (* not an error *) ""
+ | e -> (* unmanaged error *)
+ "<error>" ^
+ (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false ()
+ (Printexc.to_string e)) ^ "</error>"
+ in
+
+ let rec aux acc text =
+ try
+ prerr_endline ("evaluating: " ^ first_line text);
+ let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in
+ aux ((plen,new_parsed)::acc) new_unparsed
+ with e -> acc, error_msg e
+ (* DON'T SERIALIZE NOW!!!
+ let status = MatitaAuthentication.get_status sid in
+ GrafiteTypes.Serializer.serialize
+ ~baseuri:(NUri.uri_of_string status#baseuri) status;
+ acc, error_msg e *)
+ 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 len_parsedlist, err_msg = aux [] text in
+ let status = MatitaAuthentication.get_status sid in
+ let txt = output_status status in
+ let parsed_tag (len,txt) =
+ "<parsed length=\"" ^ (string_of_int len) ^ "\">" ^ txt ^ "</parsed>"
+ in
+ (* List.rev: the list begins with the older parsed txt *)
+ let body =
+ "<response>" ^
+ String.concat "" (List.rev (List.map parsed_tag len_parsedlist)) ^
+ txt ^ err_msg ^ "</response>"
+ in
+ (* prerr_endline ("sending goto bottom response:\n" ^ body); *)
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string body;
+(* with Not_found -> cgi#set_header ~status:`Internal_server_error
+ ~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
+ prerr_endline "gototop prima della time travel";
+ (* NCicLibrary.time_travel new_status; *)
+ prerr_endline "gototop dopo della time travel";
+ 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
+ (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 history = MatitaAuthentication.get_history sid in
+ let old_status = MatitaAuthentication.get_status sid in
+ let new_history,new_status =
+ match history with
+ _::(status::_ as history) ->
+ history, status
+ | [_] -> (prerr_endline "singleton";failwith "retract")
+ | _ -> (prerr_endline "nil"; assert false) in
+(* prerr_endline "timestamp prima della retract";
+ old_status#print_timestamp ();
+ prerr_endline "timestamp della retract";
+ new_status#print_timestamp ();
+ prerr_endline ("prima della time travel"); *)
+ NCicLibrary.time_travel new_status;
+ prerr_endline ("dopo della time travel");
+ MatitaAuthentication.set_history sid new_history;
+ MatitaAuthentication.set_status sid new_status;
+ prerr_endline ("baseuri after retract = " ^ new_status#baseuri);
+ let body = output_status new_status in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string body
+ with e ->
+ prerr_endline ("error in retract: " ^ Printexc.to_string e);
+ cgi#set_header ~status:`Internal_server_error
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\"" ());
+ cgi#out_channel#commit_work()