X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FmatitaFilesystem.ml;h=43fb985b984d2f1fda6a4539a5c6b437dacd496c;hb=f12c76e8d705aa44da328461874532e87c7fc57a;hp=1ead03f9045ec9c78a6c9b3add4f6e4c2a351a7b;hpb=fbfbf719113cb85cf49fd41d29570fe9ab47271e;p=helm.git diff --git a/matitaB/matita/matitaFilesystem.ml b/matitaB/matita/matitaFilesystem.ml index 1ead03f90..43fb985b9 100644 --- a/matitaB/matita/matitaFilesystem.ml +++ b/matitaB/matita/matitaFilesystem.ml @@ -25,6 +25,10 @@ exception SvnError of string;; +let mutex = Mutex.create ();; + +let to_be_committed = ref [];; + let exec_process cmd = let (stdout, stdin, stderr) as chs = Unix.open_process_full cmd [||] in let outlines = ref [] in @@ -48,6 +52,8 @@ let exec_process cmd = errno, output ^ "\n\n" ^ errors | _ -> assert false)) +(* this should be executed only for a freshly created user + * so no CS is needed *) let checkout user = let rt_dir = Helm_registry.get "matita.rt_base_dir" in let repo = Helm_registry.get "matita.weblib" in @@ -64,27 +70,27 @@ let html_of_library uid = let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid in - let branch text acc = + let branch lpath children = let id = newid () in - let name = Filename.basename text in + let name = Filename.basename lpath in let name = if name <> "." then name else "cic:/matita" in - "\n" ^ + "\n" ^ "\n" ^ name ^ "
\n" ^ "\n" ^ - acc ^ "\n" + children ^ "\n
" in - let leaf text = + let leaf lpath = "\n" ^ - "" ^ - (Filename.basename text) ^ "
" + "" ^ + (Filename.basename lpath) ^ "
" in let rec aux path = let lpath filename = path ^ "/" ^ filename in let gpath filename = basedir ^ "/" ^ path ^ "/" ^ filename in let dirlist = - List.filter (fun x -> String.sub x 0 1 = ".") + List.filter (fun x -> String.sub x 0 1 <> ".") (Array.to_list (Sys.readdir (basedir ^ "/" ^ path))) in let subdirs = List.filter (fun x -> Sys.is_directory (gpath x)) dirlist in let scripts = @@ -92,13 +98,14 @@ let html_of_library uid = try let i = String.rindex x '.' in let len = String.length x - i in - not (Sys.is_directory (gpath x)) && (String.sub x i len = ".ma") + not (Sys.is_directory (gpath x)) && + (String.sub x 0 1 <> ".") && (String.sub x i len = ".ma") with Not_found | Invalid_argument _ -> false) dirlist in let subdirtags = String.concat "\n" (List.map (fun x -> aux (lpath x)) subdirs) in let scripttags = String.concat "\n" - (List.map (fun x -> leaf (gpath x)) scripts) + (List.map (fun x -> leaf (lpath x)) scripts) in branch path (subdirtags ^ "\n" ^ scripttags) in @@ -107,3 +114,44 @@ let html_of_library uid = prerr_endline "BEGIN TREE";prerr_endline res;prerr_endline "END TREE"; res ;; + +let reset_lib () = + let to_be_removed = (Helm_registry.get "matita.rt_base_dir") ^ "/users/*" in + ignore (Sys.command ("rm -rf " ^ to_be_removed)) +;; + +(* adds a user to the commit queue; concurrent instances possible, so we + * enclose the update in a CS + *) +let add_user uid = + Mutex.lock mutex; + to_be_committed := uid::List.filter (fun x -> x <> uid) !to_be_committed; + Mutex.unlock mutex; +;; + +(* this function and the next one should only be called by the server itself (or + * the admin) at a scheduled time, so no concurrent instances and no CS needed + * also, svn should already be safe as far as concurrency is concerned *) +let commit user = + let rt_dir = Helm_registry.get "matita.rt_base_dir" in + let repo = Helm_registry.get "matita.weblib" in + + let errno, outstr = exec_process + ("svn ci --message \"commit by user " ^ user ^ "\" " ^ rt_dir ^ "/users/" ^ user ^ "/") + in + if errno = 0 then () + else raise (SvnError outstr) + +let do_global_commit () = + prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed); + List.fold_left + (fun acc u -> + try + commit u; + acc + with + | SvnError outstr -> + prerr_endline outstr; + u::acc) + [] (List.rev !to_be_committed) +;;