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
let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in
let outstr = ref "" in
ignore (SmallLexer.mk_small_printer interpr outstr stringbuf);
+ prerr_endline ("baseuri after advance = " ^ st#baseuri);
(* prerr_endline ("parser output: " ^ !outstr); *)
MatitaAuthentication.set_status sid st;
parsed_len,
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] (); *)
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
+ 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;
- let oc = open_out filename in
- output_string oc (locked ^ unlocked);
- close_out oc;
- if MatitaEngine.eos status unlocked then
+ 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\""
~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 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;
(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())
+ cgi#out_channel#output_string "<response>ok</response>"));
+ cgi#out_channel#commit_work()
;;
let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
history, status
| [_] -> (prerr_endline "singleton";failwith "retract")
| _ -> (prerr_endline "nil"; assert false) in
+ 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
*)
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 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
; "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