let markup =
if is_loc then
(match depth, pos with
- | 0, 0 -> "<B>" ^ (render_switch sw) ^ "</B>"
+ | 0, 0 -> "<span class=\"activegoal\">" ^ (render_switch sw) ^ "</span>"
| 0, _ ->
- Printf.sprintf "<B>|<SUB>%d</SUB>: %s</B>" pos (render_switch sw)
+ Printf.sprintf "<span class=\"activegoal\">|<SUB>%d</SUB>: %s</span>" pos (render_switch sw)
| 1, pos when Stack.head_tag s#stack = `BranchTag ->
- Printf.sprintf "|<SUB>%d</SUB> : %s" pos (render_switch sw)
+ Printf.sprintf "<span class=\"passivegoal\">|<SUB>%d</SUB> : %s</span>" pos (render_switch sw)
| _ -> 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
with
Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in
include_paths := incpaths;
- let status = MatitaAuthentication.get_status sid in
- MatitaAuthentication.set_status sid (status#set_baseuri baseuri);
+ let status = (MatitaAuthentication.get_status sid)#set_baseuri baseuri in
+ let history = [status] in
+ MatitaAuthentication.set_status sid status;
+ MatitaAuthentication.set_history sid history;
cgi # set_header
~cache:`No_cache
~content_type:"text/xml; charset=\"utf-8\""
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 ("baseuri after advance = " ^ st#baseuri);
+ (* 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
if pw = userpw then
begin
- let _ = MatitaFilesystem.html_of_library uid in
+ 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"
+(* 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
assert (cgi#arguments <> []);
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 oc = open_out filename in
- output_string oc (locked ^ unlocked);
- close_out oc;
- if MatitaEngine.eos status unlocked then
+ 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
+
+ if ((not force) && (Sys.file_exists filename)) then
+ raise File_already_exists;
+
+ if dir = "true" then
+ Unix.mkdir filename 0o744
+ else
begin
- prerr_endline ("serializing proof objects...");
- GrafiteTypes.Serializer.serialize
- ~baseuri:(NUri.uri_of_string status#baseuri) status;
- prerr_endline ("adding to the commit queue...");
- MatitaFilesystem.add_user uid;
- prerr_endline ("done.");
+ 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 ("adding to the commit queue..."); *)
+ MatitaFilesystem.add_user uid;
+ (* prerr_endline ("done."); *)
+ end;
end;
+ MatitaAuthentication.set_file_flag uid rel_filename MatitaFilesystem.MModified;
cgi # set_header
~cache:`No_cache
~content_type:"text/xml; charset=\"utf-8\""
();
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
~content_type:"text/xml; charset=\"utf-8\""
- ());
+ ()
+ | e ->
+ let estr = Printexc.to_string e in
+ cgi#out_channel#output_string ("<response>" ^ estr ^ "</response>"));
cgi#out_channel#commit_work()
;;
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
+ let files,anomalies = MatitaFilesystem.update_user uid in
+ (* let changed = HExtlib.filter_map
+ (fun (fl,n) -> if (List.mem MatitaFilesystem.Modified fl) then Some n else None) files
+ in
+ let changed = String.concat "\n" changed in
+ let anomalies = String.concat "\n" anomalies in
+ prerr_endline ("Changed:\n" ^ changed ^ "\n\nAnomalies:\n" ^ anomalies); *)
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string "<response>ok</response>"
+ 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()
+;;
+
(* 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 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
+ 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
- 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";
+ prerr_endline ("prima della time travel");
NCicLibrary.time_travel new_status;
- prerr_endline "after time travel";
+ prerr_endline ("dopo della 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));
+ prerr_endline ("baseuri after retract = " ^ new_status#baseuri);
let body = output_status new_status in
cgi # set_header
~cache:`No_cache
*)
let uid = MatitaAuthentication.user_of_session sid in
- let html = MatitaFilesystem.html_of_library uid in
+ let ft = MatitaAuthentication.read_ft uid in
+ let html = MatitaFilesystem.html_of_library uid ft in
cgi # set_header
~cache:`No_cache
~content_type:"text/html; charset=\"utf-8\""
"<script src=\"treeview/xmlTree.js\" type=\"text/javascript\"></script>\n" ^
"<body>\n" ^ *)
html (* ^ "\n</body></html>" *) );
+
+ let files,anomalies = MatitaFilesystem.stat_user uid in
+ let changed = HExtlib.filter_map
+ (fun (n,fl) -> if (List.mem MatitaFilesystem.Modified fl) then Some n else None) files
+ in
+ let changed = String.concat "\n" changed in
+ let anomalies = String.concat "\n" anomalies in
+ prerr_endline ("Changed:\n" ^ changed ^ "\n\nAnomalies:\n" ^ anomalies);
cgi#out_channel#commit_work()
;;
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;
dyn_translator = (fun _ -> ""); (* not needed *)
dyn_accept_all_conditionals = false;
} in
+ let do_update =
+ { Nethttpd_services.dyn_handler = (fun _ -> svn_update);
+ 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 nethttpd_factory =
Nethttpd_plex.nethttpd_factory
~handlers:[ "advance", do_advance
; "retract", do_retract
; "bottom", goto_bottom
+ ; "top", goto_top
; "open", retrieve
; "register", do_register
; "login", do_login
; "reset", do_resetlib
; "viewlib", do_viewlib
; "save", do_save
- ; "commit", do_commit]
+ ; "commit", do_commit
+ ; "update", do_update]
() in
MatitaInit.initialize_all ();
MatitaAuthentication.deserialize ();
projects / helm.git / blobdiff