X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=95ff43b17f852704fec42989414cda56a10cfca7;hb=fd05d5ee6ec6b74a88f1b6f25319760b4c05ba7c;hp=5abb8ad07e8f90dd03f0e718556b0127d8aa72e5;hpb=66b7f75467ba81224d961beda0ad0e55664c68b6;p=helm.git diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 5abb8ad07..95ff43b17 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -89,19 +89,17 @@ let output_status s = let markup = if is_loc then (match depth, pos with - | 0, 0 -> "" ^ (render_switch sw) ^ "" + | 0, 0 -> "" ^ (render_switch sw) ^ "" | 0, _ -> - Printf.sprintf "|_%d: %s" pos (render_switch sw) + Printf.sprintf "|_%d: %s" pos (render_switch sw) | 1, pos when Stack.head_tag s#stack = `BranchTag -> - Printf.sprintf "|_%d : %s" pos (render_switch sw) + Printf.sprintf "|_%d : %s" 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 = "" ^ markup ^ "" in - prerr_endline "pippo2"; let sequent = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw) in @@ -109,43 +107,23 @@ let output_status s = "" ^ markup ^ txt0 ^ "" ^ acc in - let res = "" ^ + "" ^ (Stack.fold ~env:(render_sequent true) ~cont:(render_sequent false) ~todo:(render_sequent false) "" s#stack) ^ "" - in - prerr_endline ("sending metasenv:\n" ^ res); res + (* prerr_endline ("sending metasenv:\n" ^ res); res *) ;; -(* let html_of_status s = - let _,_,metasenv,subst,_ = s#obj in - let txt = List.fold_left - (fun acc (nmeta,_ as meta) -> - let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent - ~metasenv ~subst ~map_unicode_to_tex:false 80 s meta) - in - prerr_endline ("### txt0 = " ^ txt0); - ("Goal ?" ^ (string_of_int nmeta) ^ "\n" ^ txt0)::acc) - [] metasenv - in - String.concat "\n\n" txt -;; *) - 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 ;; @@ -199,13 +177,13 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (); *) 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 = "" ^ body ^ "" in let baseuri, incpaths = try @@ -222,8 +200,10 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = 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\"" @@ -253,7 +233,8 @@ let advance0 sid text = 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 @@ -269,7 +250,7 @@ let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (try MatitaAuthentication.add_user uid userpw; (* env#set_output_header_field "Location" "/index.html" *) - cgi#outchannel#output_string + cgi#out_channel#output_string ("" ^ "Redirecting to login page...") with @@ -302,20 +283,20 @@ let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = 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" *) - cgi#outchannel#output_string + cgi#out_channel#output_string ("" ^ "Redirecting to Matita page...") 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\"" @@ -351,6 +332,8 @@ let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = 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 @@ -362,26 +345,67 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = 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, Some MatitaFilesystem.MModified]; cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string "ok" with + | File_already_exists -> + cgi#out_channel#output_string "cancelled" + | 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 ("" ^ estr ^ "")); + 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 errors,out = MatitaFilesystem.do_global_commit () in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string ""; + cgi#out_channel#output_string "ok"; + cgi#out_channel#output_string "

" ^ out ^ "

"; + cgi#out_channel#output_string "" + with | Not_found _ -> cgi # set_header ~status:`Internal_server_error @@ -391,17 +415,38 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; -let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = +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 errors = MatitaFilesystem.do_global_commit () in - prerr_endline ("commit errors: " ^ (String.concat " " errors)); + 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 "ok" + cgi#out_channel#output_string ""; + cgi#out_channel#output_string "ok"; + cgi#out_channel#output_string ("

" ^ details ^ "

"); + cgi#out_channel#output_string ""; with | Not_found _ -> cgi # set_header @@ -427,7 +472,7 @@ 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); @@ -437,7 +482,7 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = new_parsed ^ "" ^ txt ^ "" 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\"" @@ -483,7 +528,7 @@ let gotoBottom (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 parsed_len, new_parsed = aux 0 "" text in let status = MatitaAuthentication.get_status sid in let txt = output_status status in @@ -496,7 +541,7 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = "" ^ txt ^ "" 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\"" @@ -508,10 +553,46 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = 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 "ok" + with _ -> + (cgi#set_header ~status:`Internal_server_error + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" (); + cgi#out_channel#output_string "ok")); + 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 @@ -528,13 +609,12 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = 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 @@ -562,7 +642,8 @@ let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = *) 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\"" @@ -575,6 +656,14 @@ let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = "\n" ^ "\n" ^ *) html (* ^ "\n" *) ); + + 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() ;; @@ -649,6 +738,13 @@ let start() = 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; @@ -705,12 +801,21 @@ let start() = 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 @@ -718,7 +823,8 @@ let start() = ; "reset", do_resetlib ; "viewlib", do_viewlib ; "save", do_save - ; "commit", do_commit] + ; "commit", do_commit + ; "update", do_update] () in MatitaInit.initialize_all (); MatitaAuthentication.deserialize ();